feat: a sequential and countably compact space is sequentially compact

Mathlib/Topology/Compactness/CountablyCompact.lean

@@ -178,16 +178,145 @@ theorem IsSeqCompact.isCountablyCompact (hA : IsSeqCompact A) :
   obtain ⟨a, ha, φ, hφ, hφa⟩ := hA.subseq_of_frequently_in hx.frequently
   exact ⟨a, ha, hφa.mapClusterPt.of_comp hφ.tendsto_atTop⟩
 
+/-- The continuous image of a countably compact set is countably compact. -/
+theorem IsCountablyCompact.image (hA : IsCountablyCompact A)
+    {f : E → F} (hf : Continuous f) : IsCountablyCompact (f '' A) := by
+  intro l hl_nebot hl_count hle
+  have : NeBot (l.comap f ⊓ 𝓟 A) :=
+    comap_inf_principal_neBot_of_image_mem hl_nebot (le_principal_iff.mp hle)
+  obtain ⟨x, hxA, hx⟩ := hA (f := l.comap f ⊓ 𝓟 A) inf_le_right
+  have := (hx.mono inf_le_left).neBot
+  exact ⟨f x, mem_image_of_mem f hxA, (hf.continuousAt.inf tendsto_comap).neBot⟩
+
+/-- If `f : X → Y` is an inducing map, the image `f '' s` of a set `s` is countably compact if and
+only if `s` is countably compact. -/
+theorem Topology.IsInducing.isCountablyCompact_iff {f : E → F} (hf : IsInducing f) :
+    IsCountablyCompact A ↔ IsCountablyCompact (f '' A) := by
+  refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot Fc F_le => ?_⟩
+  obtain ⟨_, ⟨x, x_in : x ∈ A, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
+    hs ((map_mono F_le).trans_eq map_principal)
+  exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩
+
+/-- If `f : X → Y` is an embedding, the image `f '' s` of a set `s` is countably compact if and
+only if `s` is countably compact. -/
+theorem Topology.IsEmbedding.isCountablyCompact_iff {f : E → F} (hf : IsEmbedding f) :
+    IsCountablyCompact A ↔ IsCountablyCompact (f '' A) :=
+  hf.isInducing.isCountablyCompact_iff
+
+theorem Subtype.isCountablyCompact_iff {p : E → Prop} {A : Set { x // p x }} :
+    IsCountablyCompact A ↔ IsCountablyCompact ((↑) '' A : Set E) :=
+  IsEmbedding.subtypeVal.isCountablyCompact_iff
+
+theorem isCountablyCompact_iff_isCountablyCompact_univ :
+    IsCountablyCompact A ↔ IsCountablyCompact (univ : Set A) := by
+  rw [Subtype.isCountablyCompact_iff, image_univ, Subtype.range_coe]
+
+theorem isCountablyCompact_univ_iff : IsCountablyCompact (univ : Set E) ↔ CountablyCompactSpace E :=
+  ⟨fun h => ⟨h⟩, fun h => h.1⟩
+
+theorem isCountablyCompact_iff_countablyCompactSpace :
+    IsCountablyCompact A ↔ CountablyCompactSpace A :=
+  isCountablyCompact_iff_isCountablyCompact_univ.trans isCountablyCompact_univ_iff
+
+/-- If `x : ℕ → E` has no convergent subsequence, then `⋃ i, closure {x i}` is closed. -/
+private lemma isClosed_of_not_tendsto {x : ℕ → E} [SequentialSpace E]
+    (hx : ∀ (l : E) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)) :
+    IsClosed (⋃ i, closure {x i}) := by
+  refine IsSeqClosed.isClosed fun y l hy hy' => ?_
+  by_cases! hm : ∃ m, ∃ᶠ n in atTop, y n ∈ closure {x m}
+  · obtain ⟨m, pm⟩ := hm
+    exact subset_iUnion _ m (isClosed_closure.mem_of_frequently_of_tendsto pm hy')
+  · have (j : ℕ) : ∃ᶠ k in atTop, ∃ n ≥ j, y n ∈ closure {x k} := by
+      refine frequently_atTop.2 fun a => ?_
+      have := (Filter.eventually_all_finite (by simp : (Iic a).Finite)).2 fun i hi => hm i
+      simp only [mem_Iic, eventually_atTop, ge_iff_le] at this
+      obtain ⟨c, hc⟩ := this
+      obtain ⟨b, hb⟩ := mem_iUnion.1 (hy (c + j))
+      refine ⟨b, ?_, c + j, j.le_add_left c, hb⟩
+      by_contra! hab
+      simp_all [hc (c + j) (c.le_add_right j) b hab.le]
+    obtain ⟨φ, hφ⟩ := extraction_forall_of_frequently this
+    choose ψ hψ1 hψ2 using hφ.2
+    have : Tendsto ψ atTop atTop := tendsto_atTop_mono hψ1 tendsto_id
+    refine (hx l φ hφ.1 (Tendsto.specializes (hy'.comp this) (fun n => ?_))).elim
+    exact specializes_iff_mem_closure.2 (hψ2 n)
+
+/-- If a sequential space is countably compact, then it is sequentially compact. We follow the proof
+in [kremsater1972sequential]. -/
+instance [SequentialSpace E] [CountablyCompactSpace E] :
+    SeqCompactSpace E := by
+  -- We prove by contradiction. If `E` is not sequentially compact, then there exists a sequence
+  -- `x : ℕ → E` with no convergent subsequence.
+  by_contra
+  simp only [seqCompactSpace_iff, IsSeqCompact, mem_univ, not_forall,
+    true_and, not_exists, not_and, exists_const] at this
+  obtain ⟨x, hx⟩ := this
+  -- Consider the set `A = ⋃ i, closure {x i}`. It is closed by `isClosed_of_not_tendsto` and thus
+  -- countably compact.
+  let A := ⋃ i, closure {x i}
+  have : IsCountablyCompact A :=
+    (isCountablyCompact_univ_iff.2 inferInstance).of_isClosed_subset
+      (isClosed_of_not_tendsto hx) (by simp)
+  -- We use the countably compactness of `A` to find a cluster point `a`. Eventually `a` does not
+  -- belong to the closure of `{x n}` as `x` has no convergent subsequence, and this contradicts `a`
+  -- being a cluster point.
+  obtain ⟨a, ha⟩ : ∃ a ∈ A, MapClusterPt a atTop x := by
+    refine isCountablyCompact_iff_seq_clusterPt.1 this _ (.of_forall fun n => ?_)
+    exact mem_iUnion_of_mem n <| subset_closure <| mem_singleton (x n)
+  obtain ⟨k, hk⟩ : ∃ k, ∀ n > k, a ∉ closure {x n} := by
+    by_contra!
+    obtain ⟨φ, hφ1, hφ2⟩ := Nat.exists_strictMono_subsequence this
+    refine hx a φ hφ1 (tendsto_atTop_nhds.2 fun U ha hUo => ⟨0, fun n _ => ?_⟩)
+    simpa using mem_closure_iff.1 (hφ2 n) U hUo ha
+  have : a ∉ ⋃ i, closure {x (i + (k + 1))} := by
+    simpa [← iUnion_ge_eq_iUnion_nat_add (fun n => closure {x n}) (k + 1)] using
+      fun i hi => hk i (Nat.lt_of_lt_of_eq hi rfl)
+  apply this
+  have := mapClusterPt_atTop_iff_forall_mem_closure.1 ha.2 (k + 1)
+  suffices h : closure (x '' Ici (k + 1)) ⊆ ⋃ i, closure {x (i + (k + 1))} from h this
+  refine (IsClosed.closure_subset_iff (isClosed_of_not_tendsto fun l φ hφ => ?_)).2 ?_
+  · exact hx l _ ((strictMono_id.add_const _).comp hφ)
+  · simp only [image_eq_iUnion, mem_Ici, iUnion_ge_eq_iUnion_nat_add _ (k + 1)]
+    exact iUnion_mono fun i => subset_closure
+
+/-- If `f : X → Y` is an embedding map, the image `f '' s` of a set `s` is sequentially compact
+  if and only if `s` is sequentially compact. -/
+theorem Topology.IsEmbedding.isSeqCompact_iff {f : E → F} (hf : IsEmbedding f) :
+    IsSeqCompact A ↔ IsSeqCompact (f '' A) where
+  mp hA x hx := by
+    choose y hy using hx
+    obtain ⟨a, ha, ⟨φ, hφ⟩⟩ := hA (fun n => (hy n).1)
+    refine ⟨f a, mem_image_of_mem f ha, φ, hφ.1, ?_⟩
+    suffices f ∘ y ∘ φ = x ∘ φ from this ▸ (hf.continuous.tendsto a).comp hφ.2
+    grind
+  mpr hA x hx := by
+    obtain ⟨fa, hfa, ⟨φ, hφ⟩⟩ := hA (fun n => mem_image_of_mem f (hx n))
+    choose a ha using hfa
+    exact ⟨a, ha.1, φ, hφ.1, hf.tendsto_nhds_iff.2 (ha.2 ▸ hφ.2)⟩
+
+theorem Subtype.isSeqCompact_iff {p : E → Prop} {A : Set { x // p x }} :
+    IsSeqCompact A ↔ IsSeqCompact ((↑) '' A : Set E) :=
+  IsEmbedding.subtypeVal.isSeqCompact_iff
+
+theorem isSeqCompact_iff_isSeqCompact_univ : IsSeqCompact A ↔ IsSeqCompact (univ : Set A) := by
+  rw [Subtype.isSeqCompact_iff, image_univ, Subtype.range_coe]
+
+theorem isSeqCompact_univ_iff : IsSeqCompact (univ : Set E) ↔ SeqCompactSpace E :=
+  ⟨fun h => ⟨h⟩, fun h => h.1⟩
+
+theorem isSeqCompact_iff_seqCompactSpace : IsSeqCompact A ↔ SeqCompactSpace A :=
+  isSeqCompact_iff_isSeqCompact_univ.trans isSeqCompact_univ_iff
+
 /-- A sequentially compact space is countably compact. -/
 instance instSeqCompactSpaceCountablyCompactSpace
     {X : Type*} [TopologicalSpace X] [SeqCompactSpace X] : CountablyCompactSpace X where
   isCountablyCompact_univ := isSeqCompact_univ.isCountablyCompact
 
 /-- In a first-countable space, a countably compact set is sequentially compact. -/
 theorem IsCountablyCompact.isSeqCompact [FirstCountableTopology E]
-    (hA : IsCountablyCompact A) : IsSeqCompact A := fun x hx =>
-    let ⟨a, haA, hac⟩ := IsCountablyCompact.seq_clusterPt hA x (Eventually.of_forall hx)
-    ⟨a, haA, hac.tendsto_subseq⟩
+    (hA : IsCountablyCompact A) : IsSeqCompact A :=
+  have : CountablyCompactSpace A := isCountablyCompact_iff_countablyCompactSpace.1 hA
+  isSeqCompact_iff_seqCompactSpace.2 inferInstance
 
 /-- A first-countable countably compact space is sequentially compact. -/
 instance instCountablyCompactSpaceSeqCompactSpace {X : Type*} [TopologicalSpace X]
@@ -256,16 +385,6 @@ theorem IsCountablyCompact.isCompact [HereditarilyLindelofSpace E]
     (hA : IsCountablyCompact A) : IsCompact A :=
   (HereditarilyLindelofSpace.isLindelof A).isCompact hA
 
-/-- The continuous image of a countably compact set is countably compact. -/
-theorem IsCountablyCompact.image (hA : IsCountablyCompact A)
-    {f : E → F} (hf : Continuous f) : IsCountablyCompact (f '' A) := by
-  intro l hl_nebot hl_count hle
-  have : NeBot (l.comap f ⊓ 𝓟 A) :=
-    comap_inf_principal_neBot_of_image_mem hl_nebot (le_principal_iff.mp hle)
-  obtain ⟨x, hxA, hx⟩ := hA (f := l.comap f ⊓ 𝓟 A) inf_le_right
-  have := (hx.mono inf_le_left).neBot
-  exact ⟨f x, mem_image_of_mem f hxA, (hf.continuousAt.inf (@tendsto_comap _ _ f l)).neBot⟩
-
 /-- The union of two countably compact sets is countably compact. -/
 theorem IsCountablyCompact.union (hA : IsCountablyCompact A) (hB : IsCountablyCompact B) :
     IsCountablyCompact (A ∪ B) := by

Mathlib/Topology/Inseparable.lean

@@ -93,6 +93,13 @@ theorem ker_nhds_eq_specializes : (𝓝 x).ker = {y | y ⤳ x} := by
 theorem specializes_iff_forall_open : x ⤳ y ↔ ∀ s : Set X, IsOpen s → y ∈ s → x ∈ s :=
   (specializes_TFAE x y).out 0 2
 
+omit [TopologicalSpace X] in
+theorem Tendsto.specializes {l : Filter X} {y : Y} (h : Tendsto g l (𝓝 y)) (hl : ∀ x, f x ⤳ g x) :
+    Tendsto f l (𝓝 y) := by
+  simp_all only [specializes_iff_forall_open, tendsto_nhds]
+  refine fun s ho hy => mem_of_superset (h s ho hy) fun x hx => ?_
+  exact mem_preimage.2 (hl x s ho (mem_preimage.1 hx))
+
 theorem Specializes.mem_open (h : x ⤳ y) (hs : IsOpen s) (hy : y ∈ s) : x ∈ s :=
   specializes_iff_forall_open.1 h s hs hy
 

docs/references.bib

@@ -3523,6 +3523,13 @@ @Article{         kratschmer_urusov2023
   url           = {https://doi.org/10.1007/s10959-022-01207-8}
 }
 
+@PhDThesis{       kremsater1972sequential,
+  title         = {Sequential space methods},
+  author        = {Kremsater, Terry Philip},
+  year          = {1972},
+  school        = {University of British Columbia}
+}
+
 @Book{            kung_rota_yan2009,
   author        = {Kung, Joseph P. S. and Rota, Gian-Carlo and Yan, Catherine
                   H.},