From d9118ded7681bf0c54d2d6092f90e8f2b429c83a Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sun, 3 Jan 2016 21:25:09 -0500
Subject: [PATCH] feat(library/theories/topology/basic): show that generated
 topology is initial

---
 .../measure_theory/sigma_algebra.lean         |  2 +-
 library/theories/topology/basic.lean          | 37 ++++++++++---------
 2 files changed, 21 insertions(+), 18 deletions(-)

diff --git a/library/theories/measure_theory/sigma_algebra.lean b/library/theories/measure_theory/sigma_algebra.lean
index 99a5a17b54..ab5e617518 100644
--- a/library/theories/measure_theory/sigma_algebra.lean
+++ b/library/theories/measure_theory/sigma_algebra.lean
@@ -126,7 +126,7 @@ protected theorem le_antisymm (M N : sigma_algebra X) : M ≤ N → N ≤ M →
 assume H1, assume H2,
 sigma_algebra.eq (subset.antisymm H1 H2)
 
-theorem generated_by_initial {G : set (set X)} {M : sigma_algebra X} (H : G ⊆ @sets X M) :
+protected theorem generated_by_initial {G : set (set X)} {M : sigma_algebra X} (H : G ⊆ @sets X M) :
   sigma_algebra.generated_by G ≤ M :=
 sets_generated_by_initial H
 
diff --git a/library/theories/topology/basic.lean b/library/theories/topology/basic.lean
index 2509106780..b902d2bde0 100644
--- a/library/theories/topology/basic.lean
+++ b/library/theories/topology/basic.lean
@@ -40,19 +40,6 @@ have ∀₀ t ∈ s ' univ, Open t,
     show Open t, by rewrite -Hi; exact H i,
 using this, by rewrite Union_eq_sUnion_image; apply Open_sUnion this
 
-private definition bin_ext (s t : set X) (n : ℕ) : set X :=
-nat.cases_on n s (λ m, t)
-
-private lemma Union_bin_ext (s t : set X) : (⋃ i, bin_ext s t i) = s ∪ t :=
-ext (take x, iff.intro
-  (suppose x ∈ Union (bin_ext s t),
-    obtain i (Hi : x ∈ (bin_ext s t) i), from this,
-    by cases i; apply or.inl Hi; apply or.inr Hi)
-  (suppose x ∈ s ∪ t,
-    or.elim this
-      (suppose x ∈ s, exists.intro 0 this)
-      (suppose x ∈ t, exists.intro 1 this)))
-
 theorem Open_union {s t : set X} (Hs : Open s) (Ht : Open t) : Open (s ∪ t) :=
 have ∀ i, Open (bin_ext s t i), by intro i; cases i; exact Hs; exact Ht,
 show Open (s ∪ t), using this, by rewrite -Union_bin_ext; exact Open_Union this
@@ -195,17 +182,33 @@ inductive opens_generated_by {X : Type} (B : set (set X)) : set X → Prop :=
                     opens_generated_by B (s ∩ t)
 | sUnion_mem     : ∀ ⦃S : set (set X)⦄, S ⊆ opens_generated_by B → opens_generated_by B (⋃₀ S)
 
-definition topology_generated_by [instance] [reducible] {X : Type} (B : set (set X)) : topology X :=
+protected definition generated_by [instance] [reducible] {X : Type} (B : set (set X)) : topology X :=
 ⦃topology,
   opens            := opens_generated_by B,
   univ_mem_opens   := opens_generated_by.univ_mem B,
-  sUnion_mem_opens := opens_generated_by.sUnion_mem,
-  inter_mem_opens  := λ s Hs t Ht, opens_generated_by.inter_mem Hs Ht
+  inter_mem_opens  := λ s Hs t Ht, opens_generated_by.inter_mem Hs Ht,
+  sUnion_mem_opens := opens_generated_by.sUnion_mem
 ⦄
 
 theorem generators_mem_topology_generated_by {X : Type} (B : set (set X)) :
-  let T := topology_generated_by B in
+  let T := topology.generated_by B in
   ∀₀ s ∈ B, @Open _ T s :=
 λ s H, opens_generated_by.generators_mem H
 
+theorem opens_generated_by_initial {X : Type} {B : set (set X)} {T : topology X} (H : B ⊆ @opens _ T) :
+  opens_generated_by B ⊆ @opens _ T :=
+begin
+  intro s Hs,
+  induction Hs with s sB s t os ot soX toX S SB SOX,
+    {exact H sB},
+    {exact univ_mem_opens X},
+    {exact inter_mem_opens X soX toX},
+  exact sUnion_mem_opens SOX
+end
+
+theorem topology_generated_by_initial {X : Type} {B : set (set X)} {T : topology X}
+    (H : ∀₀ s ∈ B, @Open _ T s) {s : set X} (H1 : @Open _ (topology.generated_by B) s) :
+  @Open _ T s :=
+opens_generated_by_initial H H1
+
 end topology