chore(order/bounded_order): lemmas about disjoint on prod, pi, and Pr…

…op (#17500)

Also adds `codisjoint` and `is_compl` lemmas.

src/order/bounded_order.lean

@@ -1443,7 +1443,6 @@ instance [has_le α] [has_le β] [order_bot α] [order_bot β] : order_bot (α 
 instance [has_le α] [has_le β] [bounded_order α] [bounded_order β] : bounded_order (α × β) :=
 { .. prod.order_top α β, .. prod.order_bot α β }
 
-
 end prod
 
 section linear_order
@@ -1725,7 +1724,7 @@ section is_compl
 (disjoint : disjoint x y)
 (codisjoint : codisjoint x y)
 
-lemma is_compl_iff [lattice α] [bounded_order α] {a b : α} :
+lemma is_compl_iff [partial_order α] [bounded_order α] {a b : α} :
   is_compl a b ↔ disjoint a b ∧ codisjoint a b := ⟨λ h, ⟨h.1, h.2⟩, λ h, ⟨h.1, h.2⟩⟩
 
 namespace is_compl
@@ -1813,6 +1812,67 @@ lemma inf_sup {x' y'} (h : is_compl x y) (h' : is_compl x' y') :
 
 end is_compl
 
+namespace prod
+variables [partial_order α] [partial_order β]
+
+protected lemma disjoint_iff [order_bot α] [order_bot β] {x y : α × β} :
+  disjoint x y ↔ disjoint x.1 y.1 ∧ disjoint x.2 y.2 :=
+begin
+  split,
+  { intros h,
+    refine ⟨λ a hx hy, (@h (a, ⊥) ⟨hx, _⟩ ⟨hy, _⟩).1, λ b hx hy, (@h (⊥, b) ⟨_, hx⟩ ⟨_, hy⟩).2⟩,
+    all_goals { exact bot_le }, },
+  { rintros ⟨ha, hb⟩ z hza hzb,
+    refine ⟨ha hza.1 hzb.1, hb hza.2 hzb.2⟩ },
+end
+
+protected lemma codisjoint_iff [order_top α] [order_top β] {x y : α × β} :
+  codisjoint x y ↔ codisjoint x.1 y.1 ∧ codisjoint x.2 y.2 :=
+@prod.disjoint_iff αᵒᵈ βᵒᵈ _ _ _ _ _ _
+
+protected lemma is_compl_iff [bounded_order α] [bounded_order β]
+  {x y : α × β} :
+  is_compl x y ↔ is_compl x.1 y.1 ∧ is_compl x.2 y.2 :=
+by simp_rw [is_compl_iff, prod.disjoint_iff, prod.codisjoint_iff, and_and_and_comm]
+
+end prod
+
+namespace pi
+variables {ι : Type*} {α' : ι → Type*} [Π i, partial_order (α' i)]
+
+lemma disjoint_iff [Π i, order_bot (α' i)] {f g : Π i, α' i} :
+  disjoint f g ↔ ∀ i, disjoint (f i) (g i) :=
+begin
+  split,
+  { intros h i x hf hg,
+    refine (update_le_iff.mp $
+      h (update_le_iff.mpr ⟨hf, λ _ _, _⟩) (update_le_iff.mpr ⟨hg, λ _ _, _⟩)).1,
+    { exact ⊥},
+    { exact bot_le },
+    { exact bot_le }, },
+  { intros h x hf hg i,
+    apply h i (hf i) (hg i) },
+end
+
+lemma codisjoint_iff [Π i, order_top (α' i)] {f g : Π i, α' i} :
+  codisjoint f g ↔ ∀ i, codisjoint (f i) (g i) :=
+@disjoint_iff _ (λ i, (α' i)ᵒᵈ) _ _ _ _
+
+lemma is_compl_iff [Π i, bounded_order (α' i)] {f g : Π i, α' i} :
+  is_compl f g ↔ ∀ i, is_compl (f i) (g i) :=
+by simp_rw [is_compl_iff, disjoint_iff, codisjoint_iff, forall_and_distrib]
+
+end pi
+
+@[simp] lemma Prop.disjoint_iff {P Q : Prop} : disjoint P Q ↔ ¬(P ∧ Q) := disjoint_iff_inf_le
+@[simp] lemma Prop.codisjoint_iff {P Q : Prop} : codisjoint P Q ↔ P ∨ Q :=
+codisjoint_iff_le_sup.trans $ forall_const _
+@[simp] lemma Prop.is_compl_iff {P Q : Prop} : is_compl P Q ↔ ¬(P ↔ Q) :=
+begin
+  rw [is_compl_iff, Prop.disjoint_iff, Prop.codisjoint_iff, not_iff],
+  tauto,
+end
+
 section
 variables [lattice α] [bounded_order α] {a b x : α}