...

Author: nguyenvukhang

Munkres/Basic.lean

@@ -1,4 +1,4 @@
-import Mathlib.Topology.Separation.Hausdorff
+import Mathlib.Topology.Defs.Filter
 
 universe u
 

Munkres/Defs/Subtype.lean

@@ -3,6 +3,7 @@ import Munkres.Mathlib.AccPt.Basic
 import Munkres.Mathlib.AccPt.Countable
 import Munkres.Mathlib.Continuous
 import Munkres.Mathlib.Disjoint
+import Munkres.Mathlib.IsOpen
 import Munkres.Mathlib.Lipschitz
 import Munkres.Mathlib.MonotoneSubseq
 import Munkres.Mathlib.Prelude

Munkres/Mathlib.lean

@@ -0,0 +1,67 @@
+import Munkres.Mathlib.Prelude
+
+open Set TopologicalSpace Topology
+
+universe u
+
+variable {α : Type u} {B : Set (Set α)}
+
+-- If U is a set such that (for all x ∈ U, there exists some b ∈ B such that
+-- x ∈ b ⊆ U), then U can be written as a union of B's elements.
+lemma b3d183c (U : Set α) :
+  (∀ x ∈ U, ∃ b ∈ B, x ∈ b ∧ b ⊆ U) → ∃ s ⊆ B, U = ⋃₀ s
+  := by --
+  intro h
+  let hp (x : U) : Set α := (h x x.prop).choose
+  let s := Set.range hp
+  use Set.range hp
+  refine ⟨?_, ?_⟩
+  · intro _ ⟨x, heq⟩
+    subst heq
+    exact (h x x.prop).choose_spec.1
+  · rw [Set.sUnion_range]
+    ext x : 1
+    rw [Set.mem_iUnion]
+    refine ⟨?_, ?_⟩
+    · intro hx
+      exact ⟨⟨x, hx⟩, (h x hx).choose_spec.2.1⟩
+    · intro ⟨y, hy⟩
+      exact (h y y.prop).choose_spec.2.2 hy -- ∎
+
+/-- This is how Munkres defines the topology generated by a basis.
+In particular, `𝓣 = generateFrom B` -/
+theorem IsOpen_generateFrom_iff (U : Set α)
+  (exists_subset_inter : ∀ t₁ ∈ B, ∀ t₂ ∈ B, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ B, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂)
+  (sUnion_eq : ⋃₀ B = univ)
+  : IsOpen[generateFrom B] U ↔ ∀ x ∈ U, ∃ b ∈ B, x ∈ b ∧ b ⊆ U
+  := by --
+  refine ⟨?_, ?_⟩
+  · intro h x hx
+    rw [Set.sUnion_eq_univ_iff] at sUnion_eq
+    induction h with
+    | basic b hb =>
+      exact ⟨b, hb, hx, le_rfl⟩
+    | univ =>
+      obtain ⟨b, h⟩ := sUnion_eq x
+      exact ⟨b, h.1, h.2, Set.subset_univ _⟩
+    | inter u₁ u₂ _ _ hu₁ hu₂ =>
+      obtain ⟨b₁, hb₁, hx₁, hu₁⟩ := hu₁ hx.1
+      obtain ⟨b₂, hb₂, hx₂, hu₂⟩ := hu₂ hx.2
+      specialize exists_subset_inter b₁ hb₁ b₂ hb₂ x ⟨hx₁, hx₂⟩
+      obtain ⟨b, hbB, hxb, hb⟩ := exists_subset_inter
+      refine ⟨b, hbB, hxb, ?_⟩
+      rw [Set.subset_inter_iff] at hb ⊢
+      exact ⟨hb.1.trans hu₁, hb.2.trans hu₂⟩
+    | sUnion s _ hs =>
+      obtain ⟨u, hus, hxu⟩ := hx
+      specialize hs u hus hxu
+      obtain ⟨b, hbB, hxb, hbu⟩ := hs
+      refine ⟨b, hbB, hxb, ?_⟩
+      refine hbu.trans ?_
+      exact Set.subset_sUnion_of_subset s u le_rfl hus
+  · intro h
+    obtain ⟨s, hs, heq⟩ := b3d183c U h
+    subst heq
+    refine GenerateOpen.sUnion s ?_
+    intro u hu
+    exact GenerateOpen.basic u (hs hu) -- ∎

Munkres/Mathlib/IsOpen.lean

@@ -1,17 +1,16 @@
 import Munkres.Mathlib.Prelude
+import Munkres.Mathlib.IsOpen
 
-open Set TopologicalSpace
+open Set TopologicalSpace Topology
 
 universe u
 
 variable {α : Type u} {B : Set (Set α)}
 
-section DefiningABasis
-
 -- The reason why we reduce all finite intersection arguments to just the
 -- intersection of two elements — that we can extend it to finite intersections
 -- by induction.
-example {B : Set (Set α)}
+example
   (h : ∀ b₁ ∈ B, ∀ b₂ ∈ B, b₁ ∩ b₂ ∈ B)
   (h_univ : univ ∈ B)
   : ∀ s ⊆ B, s.Finite → ⋂₀ s ∈ B
@@ -33,102 +32,56 @@ example {B : Set (Set α)}
     rw [sInter_insert u s]
     exact h u huB _ ih -- ∎
 
-variable
-  (h₁ : ∀ x, ∃ b ∈ B, x ∈ b)
-  (h₂ : ∀ b₁ ∈ B, ∀ b₂ ∈ B, ∀ x ∈ b₁ ∩ b₂, ∃ b ∈ B, x ∈ b ∧ b ⊆ b₁ ∩ b₂)
-
-private lemma l₀ {U : Set α} :
-  (∀ x ∈ U, ∃ b ∈ B, x ∈ b ∧ b ⊆ U) → ∃ s ⊆ B, U = ⋃₀ s
-  := by --
-  intro h
-  let hp (x : U) : Set α := (h x x.prop).choose
-  let s := Set.range hp
-  use Set.range hp
-  refine ⟨?_, ?_⟩
-  · intro _ ⟨x, heq⟩
-    subst heq
-    exact (h x x.prop).choose_spec.1
-  · rw [Set.sUnion_range]
-    ext x : 1
-    rw [Set.mem_iUnion]
-    refine ⟨?_, ?_⟩
-    · intro hx
-      exact ⟨⟨x, hx⟩, (h x hx).choose_spec.2.1⟩
-    · intro ⟨y, hy⟩
-      exact (h y y.prop).choose_spec.2.2 hy -- ∎
-
-include h₁ h₂ in
-private lemma l₁
-  : ∀ U, @IsOpen α (generateFrom B) U → ∀ x ∈ U, ∃ b ∈ B, x ∈ b ∧ b ⊆ U
-  := by --
-  intro U h x hx
-  induction h with
-  | basic b hb =>
-    exact ⟨b, hb, hx, le_rfl⟩
-  | univ =>
-    obtain ⟨b, h⟩ := h₁ x
-    exact ⟨b, h.1, h.2, Set.subset_univ _⟩
-  | inter u₁ u₂ _ _ hu₁ hu₂ =>
-    obtain ⟨b₁, hb₁, hx₁, hu₁⟩ := hu₁ hx.1
-    obtain ⟨b₂, hb₂, hx₂, hu₂⟩ := hu₂ hx.2
-    specialize h₂ b₁ hb₁ b₂ hb₂ x ⟨hx₁, hx₂⟩
-    obtain ⟨b, hbB, hxb, hb⟩ := h₂
-    refine ⟨b, hbB, hxb, ?_⟩
-    rw [Set.subset_inter_iff] at hb ⊢
-    exact ⟨hb.1.trans hu₁, hb.2.trans hu₂⟩
-  | sUnion s _ hs =>
-    obtain ⟨u, hus, hxu⟩ := hx
-    specialize hs u hus hxu
-    obtain ⟨b, hbB, hxb, hbu⟩ := hs
-    refine ⟨b, hbB, hxb, ?_⟩
-    refine hbu.trans ?_
-    exact Set.subset_sUnion_of_subset s u le_rfl hus -- ∎
-
-private lemma l₂
-  : ∀ U, (∀ x ∈ U, ∃ b ∈ B, x ∈ b ∧ b ⊆ U) → @IsOpen α (generateFrom B) U
+-- Same as the above, except that we swap out the requirement that univ ∈ B for
+-- the constraint that we're talking only about non-empty intersections.
+example
+  (h : ∀ b₁ ∈ B, ∀ b₂ ∈ B, b₁ ∩ b₂ ∈ B)
+  : ∀ s ⊆ B, s.Finite → s.Nonempty → ⋂₀ s ∈ B
   := by --
-  intro U h
-  obtain ⟨s, hs, heq⟩ := l₀ h
-  subst heq
-  refine GenerateOpen.sUnion s ?_
-  intro u hu
-  refine GenerateOpen.basic u ?_
-  exact hs hu -- ∎
-
-include h₁ h₂ in
-/-- Here's how Munkres defines the topology generated by a basis. In particular,
-`T = generateFrom B` -/
-private lemma l₃ {U : Set α}
-  : @IsOpen α (generateFrom B) U ↔ ∀ x ∈ U, ∃ b ∈ B, x ∈ b ∧ b ⊆ U
-  := ⟨l₁ h₁ h₂ U, l₂ U⟩
-
-end DefiningABasis
+  intro s hsB hsF hs₀
+  induction s, hsF using Set.Finite.induction_on with
+  | empty =>
+    rw [sInter_empty]
+    exact False.elim (Set.not_nonempty_empty hs₀)
+  | @insert u s hus hsF ih =>
+    have huB : u ∈ B := hsB <| mem_insert u s
+    if hs₀ : s = ∅ then
+      subst hs₀
+      simp only [insert_empty_eq, sInter_singleton]
+      exact huB
+    else
+    replace hs₀ : s.Nonempty := nonempty_iff_ne_empty.mpr hs₀
+    specialize ih ((subset_insert u s).trans hsB)
+    rw [sInter_insert u s]
+    exact h u huB _ (ih hs₀) -- ∎
 
 section S₁
 --* Lemma 13.1
-variable [TopologicalSpace α] (hB : IsTopologicalBasis B)
+variable [TopologicalSpace α]
 
 -- In other words, 𝓣 = collection of all unions of elements of 𝓑.
-example {U : Set α} : IsOpen U ↔ ∃ s ⊆ B, U = ⋃₀ s  := by
+example {U : Set α} (hB : IsTopologicalBasis B) : IsOpen U ↔ ∃ s ⊆ B, U = ⋃₀ s
+  := by --
   refine ⟨?_, ?_⟩
   · intro hU
     rw [hB.isOpen_iff] at hU
-    exact l₀ hU
+    exact b3d183c U hU
   · intro ⟨s, hs, heq⟩
     subst heq
     refine isOpen_sUnion ?_
     intro u hu
-    exact hB.isOpen (hs hu)
+    exact hB.isOpen (hs hu) -- ∎
 
 end S₁
 
 section S₂
 --* Lemma 13.2
-variable [TopologicalSpace α] {C : Set (Set α)}
+variable [TopologicalSpace α]
+
+example {C : Set (Set α)}
   (h₁ : ∀ c ∈ C, IsOpen c)
   (h₂ : ∀ u, IsOpen u → ∀ x ∈ u, ∃ c ∈ C, x ∈ c ∧ c ⊆ u)
-
-example : IsTopologicalBasis C
+  : IsTopologicalBasis C
   := by --
   have h₃ : ∀ x, ∃ b ∈ C, x ∈ b := by
     intro x
@@ -137,28 +90,29 @@ example : IsTopologicalBasis C
   have h₄ : ∀ s ∈ C, ∀ t ∈ C, ∀ x ∈ s ∩ t, ∃ c ∈ C, x ∈ c ∧ c ⊆ s ∩ t := by
     intro s hs t ht x hx
     exact h₂ (s ∩ t) ((h₁ s hs).inter (h₁ t ht)) x hx
+  have sUnion_eq := Set.sUnion_eq_univ_iff.mpr h₃
   exact {
-    sUnion_eq := Set.sUnion_eq_univ_iff.mpr h₃
-    exists_subset_inter := h₄
+    sUnion_eq,
+    exists_subset_inter := h₄,
     eq_generateFrom := by
       refine TopologicalSpace.ext ?_
       ext u : 2
-      rw [l₃ h₃ h₄]
+      rw [IsOpen_generateFrom_iff u h₄ sUnion_eq]
       refine ⟨h₂ u, ?_⟩
       intro h
-      obtain ⟨s, hs, heq⟩ := l₀ h
+      obtain ⟨s, hs, heq⟩ := b3d183c u h
       subst heq
       exact isOpen_sUnion fun t ht ↦ h₁ t (hs ht)
   } -- ∎
 
 end S₂
 
 section S₃
---* Lemma 13.2
+--* Lemma 13.3
 variable [T : TopologicalSpace α] [T' : TopologicalSpace α]
   {B B' : Set (Set α)}
-  (hB : IsTopologicalBasis (t := T) B)
-  (hB' : IsTopologicalBasis (t := T') B')
+  (hB : @IsTopologicalBasis _ T B)
+  (hB' : @IsTopologicalBasis _ T' B')
 
 -- Note that T' is finer than T here.
 example : T' ≤ T ↔ ∀ x, ∀ b ∈ B, x ∈ b → ∃ b' ∈ B', x ∈ b' ∧ b' ⊆ b

Munkres/Numbered/V13_BasisForATopology.lean

@@ -0,0 +1,61 @@
+import Munkres.Closure.Subtype
+import Munkres.Mathlib.AccPt.Basic
+import Munkres.Mathlib.Disjoint
+import Munkres.Subtype.Topology
+
+open Set Topology Filter TopologicalSpace
+
+universe u v
+
+variable {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β]
+
+-- Mathlib's Product Topology.
+@[reducible]
+private def tₚ : TopologicalSpace (α × β) := instTopologicalSpaceProd (X := α) (Y := β)
+
+private def B := { p | ∃ (U : Set α) (V : Set β), IsOpen U ∧ IsOpen V ∧ p = U ×ˢ V }
+
+-- private lemma l₀ {B : Set (Set α)} :
+
+example : @IsTopologicalBasis (α × β) tₚ B := by
+  set B := B (α := α) (β := β)
+  have exists_subset_inter : ∀ t₁ ∈ B, ∀ t₂ ∈ B, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ B, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
+    := by --
+    intro t₁ ⟨u₁, v₁, hu₁, hv₁, ht₁⟩ t₂ ⟨u₂, v₂, hu₂, hv₂, ht₂⟩ z ⟨hz₁, hz₂⟩
+    use (u₁ ∩ u₂) ×ˢ (v₁ ∩ v₂)
+    refine ⟨?_, ?_, ?_⟩
+    · exact ⟨u₁ ∩ u₂, v₁ ∩ v₂, hu₁.inter hu₂, hv₁.inter hv₂, rfl⟩
+    · rw [ht₁] at hz₁
+      rw [ht₂] at hz₂
+      exact mk_mem_prod ⟨hz₁.1, hz₂.1⟩ ⟨hz₁.2, hz₂.2⟩
+    · rw [prod_subset_iff]
+      intro x hx y hy
+      refine ⟨?_, ?_⟩
+      · rw [ht₁]
+        exact mk_mem_prod hx.1 hy.1
+      · rw [ht₂]
+        exact mk_mem_prod hx.2 hy.2 -- ∎
+  have sUnion_eq : ⋃₀ B = univ
+    := by --
+    refine eq_univ_of_univ_subset ?_
+    have : univ ∈ B := by
+      rw [<-univ_prod_univ]
+      exact ⟨univ, univ, isOpen_univ, isOpen_univ, rfl⟩
+    exact subset_sUnion_of_subset B univ (univ_subset_iff.mpr rfl) this -- ∎
+  have hCover : ∀ x, ∃ b ∈ B, x ∈ b := by
+    rw [<-Set.sUnion_eq_univ_iff]
+    exact sUnion_eq
+  refine { exists_subset_inter, sUnion_eq, eq_generateFrom := ?_ }
+  · refine TopologicalSpace.ext ?_
+    ext u : 2
+    refine ⟨?_, ?_⟩
+    · intro h
+      sorry
+    · sorry
+
+-- example {U : Set α} {V : Set β} (hU : IsOpen U) (hV : IsOpen V)
+--   :  := by
+--   sorry
+
+section S₀
+end S₀