docs(data/set/disjointed): add module docstring and some whitespaces (#…

…7957)

src/data/set/disjointed.lean

@@ -2,20 +2,31 @@
 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
-
-Disjointed sets
 -/
 import data.set.lattice
 import tactic.wlog
-open set classical
-open_locale classical
+
+/-!
+# Relations holding pairwise and consecutive differences of sets
+
+This file defines pairwise relations and a way to make a sequence of sets into a sequence of
+disjoint sets.
+
+## Main declarations
+
+* `pairwise p`: States that `p i j` for all `i ≠ j`.
+* `disjointed f`: Yields the sequence of sets `f 0`, `f 1 \ f 0`, `f 2 \ (f 0 ∪ f 1)`, ... This
+  sequence has the same union as `f 0`, `f 1`, `f 2` but with disjoint sets.
+
+-/
+open set
 
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x}
   {s t u : set α}
 
 /-- A relation `p` holds pairwise if `p i j` for all `i ≠ j`. -/
-def pairwise {α : Type*} (p : α → α → Prop) := ∀i j, i ≠ j → p i j
+def pairwise {α : Type*} (p : α → α → Prop) := ∀ i j, i ≠ j → p i j
 
 theorem set.pairwise_on_univ {r : α → α → Prop} :
   (univ : set α).pairwise_on r ↔ pairwise r :=
@@ -39,11 +50,11 @@ theorem pairwise_disjoint_on_bool [semilattice_inf_bot α] {a b : α} :
 pairwise_on_bool disjoint.symm
 
 theorem pairwise_on_nat {r} (hr : symmetric r) (f : ℕ → α) :
-  pairwise (r on f) ↔ (∀ (m n) (h : m < n), r (f m) (f n)) :=
+  pairwise (r on f) ↔ ∀ (m n) (h : m < n), r (f m) (f n) :=
 ⟨λ p m n w, p m n w.ne, λ p m n w, by { wlog w' : m ≤ n, exact p m n ((ne.le_iff_lt w).mp w'), }⟩
 
 theorem pairwise_disjoint_on_nat [semilattice_inf_bot α] (f : ℕ → α) :
-  pairwise (disjoint on f) ↔ (∀ (m n) (h : m < n), disjoint (f m) (f n)) :=
+  pairwise (disjoint on f) ↔ ∀ (m n) (h : m < n), disjoint (f m) (f n) :=
 pairwise_on_nat disjoint.symm f
 
 theorem pairwise.pairwise_on {p : α → α → Prop} (h : pairwise p) (s : set α) : s.pairwise_on p :=
@@ -57,42 +68,31 @@ namespace set
 /-- If `f : ℕ → set α` is a sequence of sets, then `disjointed f` is
   the sequence formed with each set subtracted from the later ones
   in the sequence, to form a disjoint sequence. -/
-def disjointed (f : ℕ → set α) (n : ℕ) : set α := f n ∩ (⋂i<n, (f i)ᶜ)
+def disjointed (f : ℕ → set α) (n : ℕ) : set α := f n ∩ (⋂ i < n, (f i)ᶜ)
 
-lemma disjoint_disjointed {f : ℕ → set α} : pairwise (disjoint on disjointed f) :=
+variables {f : ℕ → set α} {n : ℕ}
+
+lemma disjoint_disjointed : pairwise (disjoint on disjointed f) :=
 λ i j h, begin
   wlog h' : i ≤ j; [skip, {revert a, exact (this h.symm).symm}],
   rintro a ⟨⟨h₁, _⟩, h₂, h₃⟩, simp at h₃,
   exact h₃ _ (lt_of_le_of_ne h' h) h₁
 end
 
-lemma disjoint_disjointed' {f : ℕ → set α} :
+-- a more useful version might be `∀ i j x, x ∈ disjointed f i → x ∈ disjointed f j → i = j`
+lemma disjoint_disjointed' :
   ∀ i j, i ≠ j → (disjointed f i) ∩ (disjointed f j) = ∅ :=
 λ i j hij, disjoint_iff.1 $ disjoint_disjointed i j hij
 
-lemma disjointed_subset {f : ℕ → set α} {n : ℕ} : disjointed f n ⊆ f n := inter_subset_left _ _
+lemma disjointed_subset : disjointed f n ⊆ f n := inter_subset_left _ _
 
-lemma Union_lt_succ {f : ℕ → set α} {n} : (⋃i < nat.succ n, f i) = f n ∪ (⋃i < n, f i) :=
+lemma Union_lt_succ : (⋃ i < nat.succ n, f i) = f n ∪ (⋃ i < n, f i) :=
 ext $ λ a, by simp [nat.lt_succ_iff_lt_or_eq, or_and_distrib_right, exists_or_distrib, or_comm]
 
-lemma Inter_lt_succ {f : ℕ → set α} {n} : (⋂i < nat.succ n, f i) = f n ∩ (⋂i < n, f i) :=
+lemma Inter_lt_succ : (⋂ i < nat.succ n, f i) = f n ∩ (⋂ i < n, f i) :=
 ext $ λ a, by simp [nat.lt_succ_iff_lt_or_eq, or_imp_distrib, forall_and_distrib, and_comm]
 
-lemma subset_Union_disjointed {f : ℕ → set α} {n} : f n ⊆ ⋃ i < n.succ, disjointed f i :=
-λ x hx,
-  have ∃ k, x ∈ f k, from ⟨n, hx⟩,
-  have hn : ∀ (i : ℕ), i < nat.find this → x ∉ f i,
-    from assume i, nat.find_min this,
-  have hlt : nat.find this < n.succ,
-    from (nat.find_min' this hx).trans_lt n.lt_succ_self,
-  mem_bUnion hlt ⟨nat.find_spec this, mem_bInter hn⟩
-
-lemma Union_disjointed {f : ℕ → set α} : (⋃n, disjointed f n) = (⋃n, f n) :=
-subset.antisymm (Union_subset_Union $ assume i, inter_subset_left _ _)
-  (Union_subset $ λ n, subset.trans subset_Union_disjointed (bUnion_subset_Union _ _))
-
-lemma disjointed_induct {f : ℕ → set α} {n : ℕ} {p : set α → Prop}
-  (h₁ : p (f n)) (h₂ : ∀t i, p t → p (t \ f i)) :
+lemma disjointed_induct {p : set α → Prop} (h₁ : p (f n)) (h₂ : ∀ t i, p t → p (t \ f i)) :
   p (disjointed f n) :=
 begin
   rw disjointed,
@@ -104,16 +104,31 @@ begin
     exact h₂ _ n ih }
 end
 
-lemma disjointed_of_mono {f : ℕ → set α} {n : ℕ} (hf : monotone f) :
+lemma disjointed_of_mono (hf : monotone f) :
   disjointed f (n + 1) = f (n + 1) \ f n :=
-have (⋂i (h : i < n + 1), (f i)ᶜ) = (f n)ᶜ,
+have (⋂ i (h : i < n + 1), (f i)ᶜ) = (f n)ᶜ,
   from le_antisymm
     (infi_le_of_le n $ infi_le_of_le (nat.lt_succ_self _) $ subset.refl _)
-    (le_infi $ assume i, le_infi $ assume hi, compl_le_compl $ hf $ nat.le_of_succ_le_succ hi),
+    (le_infi $ λ i, le_infi $ λ hi, compl_le_compl $ hf $ nat.le_of_succ_le_succ hi),
 by simp [disjointed, this, diff_eq]
 
-lemma Union_disjointed_of_mono {f : ℕ → set α} (hf : monotone f) (n : ℕ) :
-  (⋃i<n.succ, disjointed f i) = f n :=
+open_locale classical
+
+lemma subset_Union_disjointed : f n ⊆ ⋃ i < n.succ, disjointed f i :=
+λ x hx,
+  have ∃ k, x ∈ f k, from ⟨n, hx⟩,
+  have hn : ∀ (i : ℕ), i < nat.find this → x ∉ f i,
+    from λ i, nat.find_min this,
+  have hlt : nat.find this < n.succ,
+    from (nat.find_min' this hx).trans_lt n.lt_succ_self,
+  mem_bUnion hlt ⟨nat.find_spec this, mem_bInter hn⟩
+
+lemma Union_disjointed : (⋃ n, disjointed f n) = (⋃ n, f n) :=
+subset.antisymm (Union_subset_Union $ λ i, inter_subset_left _ _)
+  (Union_subset $ λ n, subset.trans subset_Union_disjointed (bUnion_subset_Union _ _))
+
+lemma Union_disjointed_of_mono (hf : monotone f) (n : ℕ) :
+  (⋃ i < n.succ, disjointed f i) = f n :=
 subset.antisymm (bUnion_subset $ λ k hk, subset.trans disjointed_subset $ hf $ nat.lt_succ_iff.1 hk)
   subset_Union_disjointed