feat(order/complete_boolean_algebra): lemmas about binfi (#10852)

Adds corresponding `binfi` and `Inf` lemmas for existing `infi` results, especially where `rw` struggles to achieve the same thing alone.

Author: b-mehta

src/order/complete_boolean_algebra.lean

@@ -64,6 +64,22 @@ theorem infi_sup_eq (f : ι → α) (a : α) : (⨅ i, f i) ⊔ a = ⨅ i, f i 
 theorem sup_infi_eq (a : α) (f : ι → α) : a ⊔ (⨅ i, f i) = ⨅ i, a ⊔ f i :=
 @inf_supr_eq (order_dual α) _ _ _ _
 
+theorem bsupr_inf_eq {p : α → Prop} {f : Π i (hi : p i), α} (a : α) :
+  (⨆ i hi, f i hi) ⊓ a = ⨆ i hi, f i hi ⊓ a :=
+by simp only [supr_inf_eq]
+
+theorem inf_bsupr_eq (a : α) {p : α → Prop} {f : Π i (hi : p i), α} :
+  a ⊓ (⨆ i hi, f i hi) = ⨆ i hi, a ⊓ f i hi :=
+by simp only [inf_supr_eq]
+
+theorem binfi_sup_eq {p : α → Prop} {f : Π i (hi : p i), α} (a : α) :
+  (⨅ i hi, f i hi) ⊔ a = ⨅ i hi, f i hi ⊔ a :=
+@bsupr_inf_eq (order_dual α) _ _ _ _
+
+theorem sup_binfi_eq (a : α) {p : α → Prop} {f : Π i (hi : p i), α} :
+  a ⊔ (⨅ i hi, f i hi) = ⨅ i hi, a ⊔ f i hi :=
+@inf_bsupr_eq (order_dual α) _ _ _ _
+
 instance pi.complete_distrib_lattice {ι : Type*} {π : ι → Type*}
   [∀ i, complete_distrib_lattice (π i)] : complete_distrib_lattice (Π i, π i) :=
 { infi_sup_le_sup_Inf := λ a s i,

src/order/galois_connection.lean

@@ -357,23 +357,46 @@ lemma l_supr_u [complete_lattice α] [complete_lattice β] (gi : galois_insertio
 calc l (⨆ (i : ι), u (f i)) = ⨆ (i : ι), l (u (f i)) : gi.gc.l_supr
                         ... = ⨆ (i : ι), f i : congr_arg _ $ funext $ λ i, gi.l_u_eq (f i)
 
+lemma l_bsupr_u [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
+  {ι : Sort x} {p : ι → Prop} (f : Π i (hi : p i), β) :
+  l (⨆ i hi, u (f i hi)) = ⨆ i hi, f i hi :=
+by simp only [supr_subtype', gi.l_supr_u]
+
+lemma l_Sup_u_image [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
+  (s : set β) : l (Sup (u '' s)) = Sup s :=
+by rw [Sup_image, gi.l_bsupr_u, Sup_eq_supr]
+
 lemma l_inf_u [semilattice_inf α] [semilattice_inf β] (gi : galois_insertion l u) (a b : β) :
   l (u a ⊓ u b) = a ⊓ b :=
 calc l (u a ⊓ u b) = l (u (a ⊓ b)) : congr_arg l gi.gc.u_inf.symm
                ... = a ⊓ b : by simp only [gi.l_u_eq]
 
 lemma l_infi_u [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
   {ι : Sort x} (f : ι → β) :
-  l (⨅ i, u (f i)) = ⨅ i, (f i) :=
+  l (⨅ i, u (f i)) = ⨅ i, f i :=
 calc l (⨅ (i : ι), u (f i)) = l (u (⨅ (i : ι), (f i))) : congr_arg l gi.gc.u_infi.symm
                         ... = ⨅ (i : ι), f i : gi.l_u_eq _
 
+lemma l_binfi_u [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
+  {ι : Sort x} {p : ι → Prop} (f : Π i (hi : p i), β) :
+  l (⨅ i hi, u (f i hi)) = ⨅ i hi, f i hi :=
+by simp only [infi_subtype', gi.l_infi_u]
+
+lemma l_Inf_u_image [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
+  (s : set β) : l (Inf (u '' s)) = Inf s :=
+by rw [Inf_image, gi.l_binfi_u, Inf_eq_infi]
+
 lemma l_infi_of_ul_eq_self [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
   {ι : Sort x} (f : ι → α) (hf : ∀ i, u (l (f i)) = f i) :
-  l (⨅ i, (f i)) = ⨅ i, l (f i) :=
+  l (⨅ i, f i) = ⨅ i, l (f i) :=
 calc l (⨅ i, (f i)) =  l ⨅ (i : ι), (u (l (f i))) : by simp [hf]
                 ... = ⨅ i, l (f i) : gi.l_infi_u _
 
+lemma l_binfi_of_ul_eq_self [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
+  {ι : Sort x} {p : ι → Prop} (f : Π i (hi : p i), α) (hf : ∀ i hi, u (l (f i hi)) = f i hi) :
+  l (⨅ i hi, f i hi) = ⨅ i hi, l (f i hi) :=
+by { rw [infi_subtype', infi_subtype'], exact gi.l_infi_of_ul_eq_self _ (λ _, hf _ _) }
+
 lemma u_le_u_iff [preorder α] [preorder β] (gi : galois_insertion l u) {a b} :
   u a ≤ u b ↔ a ≤ b :=
 ⟨λ h, (gi.le_l_u _).trans (gi.gc.l_le h),
@@ -537,6 +560,10 @@ lemma u_infi_l [complete_lattice α] [complete_lattice β] (gi : galois_coinsert
   u (⨅ i, l (f i)) = ⨅ i, (f i) :=
 gi.dual.l_supr_u _
 
+lemma u_Inf_l_image [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u)
+  (s : set α) : u (Inf (l '' s)) = Inf s :=
+gi.dual.l_Sup_u_image _
+
 lemma u_sup_l [semilattice_sup α] [semilattice_sup β] (gi : galois_coinsertion l u) (a b : α) :
   u (l a ⊔ l b) = a ⊔ b :=
 gi.dual.l_inf_u _ _
@@ -546,11 +573,25 @@ lemma u_supr_l [complete_lattice α] [complete_lattice β] (gi : galois_coinsert
   u (⨆ i, l (f i)) = ⨆ i, (f i) :=
 gi.dual.l_infi_u _
 
+lemma u_bsupr_l [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u)
+  {ι : Sort x} {p : ι → Prop} (f : Π i (hi : p i), α) :
+  u (⨆ i hi, l (f i hi)) = ⨆ i hi, f i hi :=
+gi.dual.l_binfi_u _
+
+lemma u_Sup_l_image [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u)
+  (s : set α) : u (Sup (l '' s)) = Sup s :=
+gi.dual.l_Inf_u_image _
+
 lemma u_supr_of_lu_eq_self [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u)
   {ι : Sort x} (f : ι → β) (hf : ∀ i, l (u (f i)) = f i) :
   u (⨆ i, (f i)) = ⨆ i, u (f i) :=
 gi.dual.l_infi_of_ul_eq_self _ hf
 
+lemma u_bsupr_of_lu_eq_self [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u)
+  {ι : Sort x} {p : ι → Prop} (f : Π i (hi : p i), β) (hf : ∀ i hi, l (u (f i hi)) = f i hi) :
+  u (⨆ i hi, f i hi) = ⨆ i hi, u (f i hi) :=
+gi.dual.l_binfi_of_ul_eq_self _ hf
+
 lemma l_le_l_iff [preorder α] [preorder β] (gi : galois_coinsertion l u) {a b} :
   l a ≤ l b ↔ a ≤ b :=
 gi.dual.u_le_u_iff