Add monotone subseq

Author: nguyenvukhang

Makefile

@@ -14,6 +14,8 @@ check: generate
 generate:
 	slope generate Munkres.Defs
 	slope generate Munkres.Mathlib
+	slope generate Munkres.Mathlib.Set
+	slope generate Munkres.Mathlib.AccPt
 
 sorry:
 	rg sorry -t lean --colors 'match:fg:yellow' --colors 'line:fg:white'

Munkres/Closure/Properties.lean

@@ -0,0 +1,66 @@
+import Mathlib.Algebra.Order.Archimedean.Basic
+import Mathlib.Algebra.Order.Ring.Star
+import Mathlib.Topology.Bases
+import Munkres.Mathlib.Disjoint
+
+open Topology Filter TopologicalSpace
+
+universe u
+
+variable {α : Type u} [TopologicalSpace α] {A : Set α} {x : α} {B : Set (Set α)}
+
+--* Theorem 17.5(a): equivalence for mem_closure. Mathlib's `mem_closure_iff`.
+example : x ∈ closure A ↔ ∀ U, IsOpen U → x ∈ U → (U ∩ A).Nonempty
+  := by --
+  refine not_iff_not.mp ⟨?_, ?_⟩
+  · intro h
+    push_neg
+    refine ⟨(closure A)ᶜ, isClosed_closure.isOpen_compl, h, ?_⟩
+    refine Disjoint.inter_eq ?_
+    rw [Set.disjoint_compl_left_iff_subset]
+    exact subset_closure
+  · intro h
+    push_neg at h
+    obtain ⟨U, hU, hxU, hd⟩ := h
+    have : IsClosed Uᶜ := hU.isClosed_compl
+    have : A ⊆ Uᶜ := (Disjoint.tfae.out 0 3).mp hd
+    have : closure A ⊆ Uᶜ := (hU.isClosed_compl.closure_subset_iff).mpr this
+    exact (this · hxU) -- ∎
+
+example : x ∈ closure A ↔ ∀ U, IsOpen U → x ∈ U → (U ∩ A).Nonempty
+  := by --
+  rw [mem_closure_iff] -- ∎
+
+--* Theorem 17.5(b). Mathlib's `IsTopologicalBasis.mem_closure_iff`.
+example (hB : IsTopologicalBasis B) : x ∈ closure A ↔ ∀ b ∈ B, x ∈ b → (b ∩ A).Nonempty
+  := by --
+  rw [mem_closure_iff]
+  constructor
+  · intro h b hbB hxb
+    have : IsOpen b := hB.isOpen hbB
+    exact h b this hxb
+  · intro h u hu hxu
+    rw [hB.isOpen_iff] at hu
+    obtain ⟨b, hbB, hxb, hbu⟩ := hu x hxu
+    exact (h b hbB hxb).mono (Set.inter_subset_inter_left A hbu) -- ∎
+
+example (hB : IsTopologicalBasis B) : x ∈ closure A ↔ ∀ b ∈ B, x ∈ b → (b ∩ A).Nonempty
+  := by --
+  exact hB.mem_closure_iff -- ∎
+
+section Tendsto
+-- If a sequence converges to a point x, then that point x is in the closure of
+-- the set containing that sequence.
+variable (f : ℕ → α) (h : Tendsto f atTop (𝓝 x))
+
+example (hf : ∀ i, f i ∈ A) : x ∈ closure A
+  := by --
+  have : ∀ᶠ n in atTop, f n ∈ A := Eventually.of_forall hf
+  exact mem_closure_of_tendsto h this -- ∎
+
+example : x ∈ closure (Set.range f)
+  := by --
+  have : ∀ᶠ n in atTop, f n ∈ Set.range f := Eventually.of_forall Set.mem_range_self
+  exact mem_closure_of_tendsto h this -- ∎
+
+end Tendsto

Munkres/Closure/Subtype.lean

@@ -0,0 +1,26 @@
+import Mathlib.Topology.Constructions
+import Munkres.Mathlib.Set.As
+
+universe u
+
+variable {α : Type u} [TopologicalSpace α] {Y A : Set α}
+
+example (A : Set Y) {x : Y} : x ∈ closure A ↔ ↑x ∈ closure (Subtype.val '' A) := closure_subtype
+
+--* Theorem 17.4: the closure of A in Y equals (closure A) ∩ Y.
+theorem closure_subtype₂ (A : Set Y) : closure A = closure (A : Set α) ∩ Y
+  := by --
+  refine le_antisymm ?_ ?_
+  · intro x hx
+    rw [Subtype.coe_image] at hx
+    obtain ⟨hxY, hx⟩ := hx
+    exact ⟨closure_subtype.mp hx, hxY⟩
+  · intro x ⟨hx, hxY⟩
+    exact ⟨⟨x, hxY⟩, closure_subtype.mpr hx, rfl⟩ -- ∎
+
+--* Theorem 17.4: If A ⊆ Y, the closure of A in Y equals (closure A) ∩ Y.
+theorem closure_subtype₃ {hAY : A ⊆ Y} : closure (A.as Y) = closure A ∩ Y
+  := by --
+  rw [closure_subtype₂ (A.as Y)]
+  refine congrArg (closure · ∩ Y) ?_
+  exact Set.as_subtype_subset_eq hAY -- ∎

Munkres/Defs.lean

@@ -6,6 +6,7 @@ import Munkres.Defs.IsBasisAt
 import Munkres.Defs.IsSaturated
 import Munkres.Defs.Metric.Basic
 import Munkres.Defs.OpenCover
+import Munkres.Defs.Separation
 import Munkres.Defs.Subspace
 import Munkres.Defs.Subtype
 set_option linter.style.longLine false

Munkres/Defs/Separation.lean

@@ -0,0 +1,16 @@
+import Mathlib.Data.Set.BooleanAlgebra
+import Mathlib.Order.CompletePartialOrder
+import Mathlib.Topology.Defs.Basic
+
+universe u
+
+variable {α : Type u} [TopologicalSpace α]
+
+/-- The existence of a separation implies that a space is not connected. -/
+structure IsSeparation (U V : Set α) : Prop where
+  left' : IsOpen U ∧ U.Nonempty
+  right' : IsOpen V ∧ V.Nonempty
+  disjoint' : Disjoint U V
+  union' : U ∪ V = Set.univ
+
+def HasSeparation (α : Type u) [TopologicalSpace α] : Prop := ∃ U V : Set α, IsSeparation U V

Munkres/Disjoint.lean

@@ -0,0 +1,26 @@
+import Munkres.Mathlib.Disjoint
+import Munkres.Mathlib.Prelude
+import Munkres.Closure.Subtype
+
+universe u
+
+variable {α : Type u} [TopologicalSpace α]
+
+section SubspaceTopology
+
+variable {X : Set α} {A B : Set X}
+
+/-- If A and B are disjoint and A is closed, then
+A = closure A ∩ X ↔ Disjoint (closure A) B,
+where both closures are in the superspace. -/
+theorem Disjoint.eq_closure_iff_disjoint (hAB : Disjoint A B) (hA : IsClosed A)
+  : A = closure (Subtype.val '' A) ∩ X ↔
+  Disjoint (closure (Subtype.val '' A)) (Subtype.val '' B)
+  := by --
+  rw [<-Set.image_val_inter_self_right_eq_coe (D := B), <-disjoint_assoc₂]
+  refine ⟨(· ▸ Set.disjoint_image_subtype_iff.mpr hAB), ?_⟩
+  intro h'
+  rw [<-closure_subtype₂ A, Set.image_val_inj]
+  exact hA.closure_eq.symm -- ∎
+
+end SubspaceTopology

Munkres/Mathlib.lean

@@ -1,7 +1,12 @@
 import Munkres.Mathlib.AccPt
+import Munkres.Mathlib.AccPt.Basic
+import Munkres.Mathlib.AccPt.Countable
+import Munkres.Mathlib.Disjoint
 import Munkres.Mathlib.Lipschitz
 import Munkres.Mathlib.MonotoneSubseq
 import Munkres.Mathlib.Prelude
+import Munkres.Mathlib.Set
+import Munkres.Mathlib.Set.As
 import Munkres.Mathlib.Subtype
 set_option linter.style.longLine false
 

Munkres/Mathlib/AccPt.lean

@@ -1,122 +1,5 @@
-import Munkres.Defs.Countable
+import Munkres.Mathlib.AccPt.Basic
+import Munkres.Mathlib.AccPt.Countable
+set_option linter.style.longLine false
 
-open Filter Set Munkres
-open scoped Topology
-
-universe u v
-
-variable {α : Type u} [TopologicalSpace α]
-  {β : Type v}
-  {A : Set α} {x : α}
-
-/-- Munkres defines that x is a limit point of A if every open U ⊆ X containing
-x intersects with A \ {x}. This is equivalent to Mathlib's `AccPt x (𝓟 A)`. -/
-protected theorem AccPt.iff {x : α} : AccPt x (𝓟 A) ↔ ∀ U ∈ nhds' x, (U ∩ (A \ {x})).Nonempty
-  := by --
-  rw [accPt_principal_iff_clusterPt, clusterPt_principal_iff]
-  simp only [mem_nhds_iff]
-  refine ⟨fun h U ⟨hU, hxU⟩ ↦ (h U ⟨U, le_refl _, hU, hxU⟩), ?_⟩
-  intro h S ⟨U, hUS, hU, hxU⟩
-  let ⟨t, htU, htA, hne⟩ := h U ⟨hU, hxU⟩
-  exact ⟨t, hUS htU, htA, hne⟩ -- ∎
-
---* closure A = A ∪ A'
-theorem AccPt.union_eq_closure : A ∪ { x | AccPt x (𝓟 A)} = closure A
-  := by --
-  refine le_antisymm ?_ ?_
-  · intro x hx
-    rcases hx with h | (h : AccPt x (𝓟 A))
-    · exact subset_closure h
-    · rw [AccPt.iff] at h
-      rw [mem_closure_iff]
-      intro U hU hxU
-      obtain ⟨t, htU, htA, htx⟩ := h U ⟨hU, hxU⟩
-      exact ⟨t, htU, htA⟩
-  · intro x hx
-    refine or_iff_not_imp_left.mpr fun h ↦ ?_
-    simp
-    refine AccPt.iff.mpr ?_
-    intro U ⟨hU, hxU⟩
-    rw [mem_closure_iff] at hx
-    obtain ⟨y, hyU, hyA⟩ := hx U hU hxU
-    have : y ≠ x := ne_of_mem_of_not_mem hyA h
-    refine ⟨y, hyU, hyA, this⟩ -- ∎
-
-theorem AccPt.mem_closure (h : AccPt x (𝓟 A)) : x ∈ closure A
-  := by --
-  exact mem_closure_iff_clusterPt.mpr h.clusterPt -- ∎
-
--- Alternative proof.
-example (h : AccPt x (𝓟 A)) : x ∈ closure A
-  := by --
-  have : x ∈ A ∪ { x | AccPt x (𝓟 A) } := Set.mem_union_right A h
-  rw [AccPt.union_eq_closure] at this
-  exact this -- ∎
-
-theorem AccPt.of_tendsto [Nonempty β] [SemilatticeSup β] {f : β → α}
-  (hA : ∀ᶠ n in atTop, f n ∈ A) (htt : Tendsto f atTop (𝓝[≠] x))
-  : AccPt x (𝓟 A)
-  := by --
-  rw [AccPt.iff]
-  intro U ⟨hU, hxU⟩
-  rw [tendsto_nhdsWithin_iff] at htt
-  obtain ⟨htt, hne⟩ := htt
-  rw [tendsto_atTop_nhds] at htt
-  rw [eventually_atTop] at hne hA
-  specialize htt U hxU hU
-  obtain ⟨N₁, htt⟩ := htt
-  obtain ⟨N₂, hne⟩ := hne
-  obtain ⟨N₃, hA⟩ := hA
-  let N := (N₁ ⊔ N₂) ⊔ N₃
-  have hN₁ : N₁ ≤ N := le_sup_left.trans le_sup_left
-  have hN₂ : N₂ ≤ N := le_sup_right.trans le_sup_left
-  have hN₃ : N₃ ≤ N := le_sup_right
-  specialize htt N hN₁
-  specialize hne N hN₂
-  specialize hA N hN₃
-  exact ⟨f N, htt, hA, hne⟩ -- ∎
-
-theorem AccPt.of_tendsto_nat {f : ℕ → α} (hA : ∀ᶠ n in atTop, f n ∈ A)
-  (htt : Tendsto f atTop (𝓝[≠] x)) : AccPt x (𝓟 A)
-  := by --
-  exact AccPt.of_tendsto hA htt -- ∎
-
--- And this is the reason why we need (𝓝[≠] x) above, and not just (𝓝 x).
-example [h₀ : Nonempty α] : ∃ (A : Set α) (x : α) (f : ℕ → α),
-  (∀ᶠ n in atTop, f n ∈ A) ∧ Tendsto f atTop (𝓝 x) ∧ ¬AccPt x (𝓟 A)
-  := by --
-  let x := h₀.some
-  refine ⟨{x}, x, fun _ ↦ x, ?_, ?_, ?_⟩
-  · exact eventually_const.mpr rfl
-  · exact tendsto_const_nhds
-  · by_contra! h
-    rw [AccPt.iff] at h
-    specialize h univ ⟨isOpen_univ, trivial⟩
-    rw [sdiff_self, bot_eq_empty, inter_empty] at h
-    exact Set.not_nonempty_empty h -- ∎
-
-theorem AccPt.exists_tendsto [h₁ : FirstCountableTopology α]
-  : AccPt x (𝓟 A) → ∃ (f : ℕ → α), (∀ n, f n ∈ A) ∧ Tendsto f atTop (𝓝 x)
-  := by --
-  intro hx
-  rw [AccPt.iff] at hx
-  rw [FirstCountableTopology.iff] at h₁
-  specialize h₁ x
-  obtain ⟨β, hβ_countable, hβx⟩ := h₁
-  haveI : Countable β := hβ_countable
-  obtain ⟨B, hB_anti, hB⟩ := hβx.exists_antitone_eq_range
-  let hδ (n : ℕ) := hx (B n) (hB.nhds' ⟨n, rfl⟩)
-  let f (n : ℕ) : α := (hδ n).some
-  use f
-  refine ⟨?_, ?_⟩
-  · intro n
-    obtain ⟨hfB : f n ∈ B n, hfA : f n ∈ A \ {x}⟩ := (hδ n).some_mem
-    exact hfA.1
-  · rw [tendsto_atTop_nhds]
-    intro U hxU hU
-    obtain ⟨b, ⟨N, heq⟩, hbU⟩ := hB.exists_mem_subset' hU hxU
-    subst heq
-    use N
-    intro n hn
-    obtain ⟨hfB : f n ∈ B n, hfA : f n ∈ A \ {x}⟩ := (hδ n).some_mem
-    exact hbU <| hB_anti hn hfB -- ∎
+-- WARNING: THIS FILE IS AUTO-GENERATED.

Munkres/Mathlib/AccPt/Basic.lean

@@ -0,0 +1,87 @@
+import Mathlib.Order.OmegaCompletePartialOrder
+import Mathlib.Topology.NhdsWithin
+import Munkres.Defs.Basic
+
+open Filter Set Munkres
+open scoped Topology
+
+universe u v
+
+variable {α : Type u} [TopologicalSpace α] {s : Set α} {x : α}
+
+/-- Munkres defines that x is a limit point of A if every open U ⊆ X containing
+x intersects with A \ {x}. This is equivalent to Mathlib's `AccPt x (𝓟 A)`. -/
+protected theorem AccPt.iff
+  : AccPt x (𝓟 s) ↔ ∀ u, IsOpen u → x ∈ u → (u ∩ (s \ {x})).Nonempty
+  := by --
+  rw [accPt_principal_iff_clusterPt, clusterPt_principal_iff]
+  refine ⟨(· · <| ·.mem_nhds ·), ?_⟩
+  intro h v hv
+  rw [mem_nhds_iff] at hv
+  obtain ⟨u, huv, hu, hxu⟩ := hv
+  exact (h u hu hxu).mono (inter_subset_inter_left _ huv) -- ∎
+
+theorem mem_closure_iff_accPt {x : α} : x ∈ closure s ↔ x ∈ s ∨ AccPt x (𝓟 s)
+  := by --
+  rw [mem_closure_iff_clusterPt]
+  exact clusterPt_principal -- ∎
+
+--* closure A = A ∪ A'
+theorem AccPt.union_eq_closure : s ∪ { x | AccPt x (𝓟 s)} = closure s
+  := by --
+  refine Set.ext fun x ↦ ?_
+  simp only [mem_closure_iff_accPt]
+  exact Eq.to_iff rfl -- ∎
+
+theorem AccPt.mem_closure (h : AccPt x (𝓟 s)) : x ∈ closure s
+  := by --
+  exact mem_closure_iff_clusterPt.mpr h.clusterPt -- ∎
+
+-- Alternative proof.
+example (h : AccPt x (𝓟 s)) : x ∈ closure s
+  := by --
+  rw [<-AccPt.union_eq_closure]
+  exact mem_union_right s h -- ∎
+
+theorem AccPt.of_tendsto {β : Type v} [Nonempty β] [SemilatticeSup β]
+  {f : β → α} (hs : ∀ᶠ n in atTop, f n ∈ s) (h : Tendsto f atTop (𝓝[≠] x))
+  : AccPt x (𝓟 s)
+  := by --
+  rw [AccPt.iff]
+  intro U hU hxU
+  rw [tendsto_nhdsWithin_iff] at h
+  obtain ⟨h, hne⟩ := h
+  rw [tendsto_atTop_nhds] at h
+  rw [eventually_atTop] at hne hs
+  specialize h U hxU hU
+  obtain ⟨N₁, h⟩ := h
+  obtain ⟨N₂, hne⟩ := hne
+  obtain ⟨N₃, hs⟩ := hs
+  let N := (N₁ ⊔ N₂) ⊔ N₃
+  have hN₁ : N₁ ≤ N := le_sup_left.trans le_sup_left
+  have hN₂ : N₂ ≤ N := le_sup_right.trans le_sup_left
+  have hN₃ : N₃ ≤ N := le_sup_right
+  specialize h N hN₁
+  specialize hne N hN₂
+  specialize hs N hN₃
+  exact ⟨f N, h, hs, hne⟩ -- ∎
+
+-- Applies to natural numbers.
+example {f : ℕ → α} (hs : ∀ᶠ n in atTop, f n ∈ s)
+  (htt : Tendsto f atTop (𝓝[≠] x)) : AccPt x (𝓟 s)
+  := by --
+  exact AccPt.of_tendsto hs htt -- ∎
+
+-- And this is the reason why we need (𝓝[≠] x) above, and not just (𝓝 x).
+example [h₀ : Nonempty α] : ∃ (A : Set α) (x : α) (f : ℕ → α),
+  (∀ᶠ n in atTop, f n ∈ A) ∧ Tendsto f atTop (𝓝 x) ∧ ¬AccPt x (𝓟 A)
+  := by --
+  let x := h₀.some
+  refine ⟨{x}, x, fun _ ↦ x, ?_, ?_, ?_⟩
+  · exact eventually_const.mpr rfl
+  · exact tendsto_const_nhds
+  · by_contra! h
+    rw [AccPt.iff] at h
+    specialize h univ isOpen_univ trivial
+    rw [sdiff_self, bot_eq_empty, inter_empty] at h
+    exact Set.not_nonempty_empty h -- ∎