docs(order/complete_boolean_algebra): add module docstring, add white…

…spaces (#8525)

src/order/complete_boolean_algebra.lean

@@ -2,11 +2,23 @@
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
-
-Theory of complete Boolean algebras.
 -/
 import order.complete_lattice
 
+/-!
+# Completely distributive lattices and Boolean algebras
+
+In this file there are definitions and an API for completely distributive lattices and completely
+distributive Boolean algebras.
+
+## Typeclasses
+
+* `complete_distrib_lattice`: Completely distributive lattices: A complete lattice whose `⊓` and `⊔`
+  distribute over `⨆` and `⨅` respectively.
+* `complete_boolean_algebra`: Completely distributive Boolean algebra: A Boolean algebra whose `⊓`
+  and `⊔` distribute over `⨆` and `⨅` respectively.
+-/
+
 set_option old_structure_cmd true
 
 universes u v w
@@ -17,8 +29,8 @@ variables {α : Type u} {β : Type v} {ι : Sort w}
   as this class includes a requirement that the lattice join
   distribute over *arbitrary* infima, and similarly for the dual. -/
 class complete_distrib_lattice α extends complete_lattice α :=
-(infi_sup_le_sup_Inf : ∀a s, (⨅ b ∈ s, a ⊔ b) ≤ a ⊔ Inf s)
-(inf_Sup_le_supr_inf : ∀a s, a ⊓ Sup s ≤ (⨆ b ∈ s, a ⊓ b))
+(infi_sup_le_sup_Inf : ∀ a s, (⨅ b ∈ s, a ⊔ b) ≤ a ⊔ Inf s)
+(inf_Sup_le_supr_inf : ∀ a s, a ⊓ Sup s ≤ (⨆ b ∈ s, a ⊓ b))
 
 section complete_distrib_lattice
 variables [complete_distrib_lattice α] {a b : α} {s t : set α}
@@ -62,31 +74,31 @@ instance pi.complete_distrib_lattice {ι : Type*} {π : ι → Type*}
       ← supr_subtype''],
   .. pi.complete_lattice }
 
-theorem Inf_sup_Inf : Inf s ⊔ Inf t = (⨅p ∈ set.prod s t, (p : α × α).1 ⊔ p.2) :=
+theorem Inf_sup_Inf : Inf s ⊔ Inf t = (⨅ p ∈ set.prod s t, (p : α × α).1 ⊔ p.2) :=
 begin
   apply le_antisymm,
   { simp only [and_imp, prod.forall, le_infi_iff, set.mem_prod],
     intros a b ha hb,
     exact sup_le_sup (Inf_le ha) (Inf_le hb) },
-  { have : ∀ a ∈ s, (⨅p ∈ set.prod s t, (p : α × α).1 ⊔ p.2) ≤ a ⊔ Inf t,
-    { assume a ha,
-      have : (⨅p ∈ set.prod s t, ((p : α × α).1 : α) ⊔ p.2) ≤
-             (⨅p ∈ prod.mk a '' t, (p : α × α).1 ⊔ p.2),
+  { have : ∀ a ∈ s, (⨅ p ∈ set.prod s t, (p : α × α).1 ⊔ p.2) ≤ a ⊔ Inf t,
+    { rintro a ha,
+      have : (⨅ p ∈ set.prod s t, ((p : α × α).1 : α) ⊔ p.2) ≤
+             (⨅ p ∈ prod.mk a '' t, (p : α × α).1 ⊔ p.2),
       { apply infi_le_infi_of_subset,
-        rintros ⟨x, y⟩,
+        rintro ⟨x, y⟩,
         simp only [and_imp, set.mem_image, prod.mk.inj_iff, set.prod_mk_mem_set_prod_eq,
                    exists_imp_distrib],
-        assume x' x't ax x'y,
+        rintro x' x't ax x'y,
         rw [← x'y, ← ax],
         simp [ha, x't] },
       rw [infi_image] at this,
       simp only at this,
       rwa ← sup_Inf_eq at this },
-    calc (⨅p ∈ set.prod s t, (p : α × α).1 ⊔ p.2) ≤ (⨅a∈s, a ⊔ Inf t) : by simp; exact this
+    calc (⨅ p ∈ set.prod s t, (p : α × α).1 ⊔ p.2) ≤ (⨅ a ∈ s, a ⊔ Inf t) : by simp; exact this
        ... = Inf s ⊔ Inf t : Inf_sup_eq.symm }
 end
 
-theorem Sup_inf_Sup : Sup s ⊓ Sup t = (⨆p ∈ set.prod s t, (p : α × α).1 ⊓ p.2) :=
+theorem Sup_inf_Sup : Sup s ⊓ Sup t = (⨆ p ∈ set.prod s t, (p : α × α).1 ⊓ p.2) :=
 @Inf_sup_Inf (order_dual α) _ _ _
 
 lemma supr_disjoint_iff {f : ι → α} : disjoint (⨆ i, f i) a ↔ ∀ i, disjoint (f i) a :=
@@ -103,7 +115,7 @@ instance complete_distrib_lattice.bounded_distrib_lattice [d : complete_distrib_
 { le_sup_inf := λ x y z, by rw [← Inf_pair, ← Inf_pair, sup_Inf_eq, ← Inf_image, set.image_pair],
   ..d }
 
-/-- A complete boolean algebra is a completely distributive boolean algebra. -/
+/-- A complete Boolean algebra is a completely distributive Boolean algebra. -/
 class complete_boolean_algebra α extends boolean_algebra α, complete_distrib_lattice α
 
 instance pi.complete_boolean_algebra {ι : Type*} {π : ι → Type*}
@@ -120,18 +132,18 @@ instance Prop.complete_boolean_algebra : complete_boolean_algebra Prop :=
 section complete_boolean_algebra
 variables [complete_boolean_algebra α] {a b : α} {s : set α} {f : ι → α}
 
-theorem compl_infi : (infi f)ᶜ = (⨆i, (f i)ᶜ) :=
+theorem compl_infi : (infi f)ᶜ = (⨆ i, (f i)ᶜ) :=
 le_antisymm
-  (compl_le_of_compl_le $ le_infi $ assume i, compl_le_of_compl_le $ le_supr (compl ∘ f) i)
-  (supr_le $ assume i, compl_le_compl $ infi_le _ _)
+  (compl_le_of_compl_le $ le_infi $ λ i, compl_le_of_compl_le $ le_supr (compl ∘ f) i)
+  (supr_le $ λ i, compl_le_compl $ infi_le _ _)
 
-theorem compl_supr : (supr f)ᶜ = (⨅i, (f i)ᶜ) :=
+theorem compl_supr : (supr f)ᶜ = (⨅ i, (f i)ᶜ) :=
 compl_injective (by simp [compl_infi])
 
-theorem compl_Inf : (Inf s)ᶜ = (⨆i∈s, iᶜ) :=
+theorem compl_Inf : (Inf s)ᶜ = (⨆ i ∈ s, iᶜ) :=
 by simp only [Inf_eq_infi, compl_infi]
 
-theorem compl_Sup : (Sup s)ᶜ = (⨅i∈s, iᶜ) :=
+theorem compl_Sup : (Sup s)ᶜ = (⨅ i ∈ s, iᶜ) :=
 by simp only [Sup_eq_supr, compl_supr]
 
 end complete_boolean_algebra