Exact source: Mathlib/Topology/Sequences.lean
Pinned GitHub source · Raw UTF-8 source
Back to A volume-normalized linear contraction obtained by a limit
1/-2Copyright (c) 2018 Jan-David Salchow. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Jan-David Salchow, Patrick Massot, Yury Kudryashov5-/6module78public import Mathlib.Topology.Defs.Sequences9public import Mathlib.Topology.Metrizable.Basic1011/-!12# Sequences in topological spaces1314In this file we prove theorems about relations15between closure/compactness/continuity etc. and their sequential counterparts.1617## Main definitions1819The following notions are defined in `Topology/Defs/Sequences`.20We build theory about these definitions here, so we remind the definitions.2122### Set operation23* `seqClosure s`: sequential closure of a set, the set of limits of sequences of points of `s`;2425### Predicates2627* `IsSeqClosed s`: predicate saying that a set is sequentially closed, i.e., `seqClosure s ⊆ s`;28* `SeqContinuous f`: predicate saying that a function is sequentially continuous, i.e.,29 for any sequence `u : ℕ → X` that converges to a point `x`, the sequence `f ∘ u` converges to30 `f x`;31* `IsSeqCompact s`: predicate saying that a set is sequentially compact, i.e., every sequence32 taking values in `s` has a converging subsequence.3334### Type classes3536* `FrechetUrysohnSpace X`: a typeclass saying that a topological space is a *Fréchet-Urysohn37 space*, i.e., the sequential closure of any set is equal to its closure.38* `SequentialSpace X`: a typeclass saying that a topological space is a *sequential space*, i.e.,39 any sequentially closed set in this space is closed. This condition is weaker than being a40 Fréchet-Urysohn space.41* `SeqCompactSpace X`: a typeclass saying that a topological space is sequentially compact, i.e.,42 every sequence in `X` has a converging subsequence.4344## Main results4546* `seqClosure_subset_closure`: closure of a set includes its sequential closure;47* `IsClosed.isSeqClosed`: a closed set is sequentially closed;48* `IsSeqClosed.seqClosure_eq`: sequential closure of a sequentially closed set `s` is equal49 to `s`;50* `seqClosure_eq_closure`: in a Fréchet-Urysohn space, the sequential closure of a set is equal to51 its closure;52* `tendsto_nhds_iff_seq_tendsto`, `FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto`: a topological53 space is a Fréchet-Urysohn space if and only if sequential convergence implies convergence;54* `FirstCountableTopology.frechetUrysohnSpace`: every topological space with55 first countable topology is a Fréchet-Urysohn space;56* `FrechetUrysohnSpace.to_sequentialSpace`: every Fréchet-Urysohn space is a sequential space;57* `IsSeqCompact.isCompact`: a sequentially compact set in a uniform space with countably58 generated uniformity is compact.5960## Tags6162sequentially closed, sequentially compact, sequential space63-/6465public section666768open Bornology Filter Function Set TopologicalSpace Topology69open scoped Uniformity7071variable {X Y : Type*}7273/-! ### Sequential closures, sequential continuity, and sequential spaces. -/7475section TopologicalSpace7677variable [TopologicalSpace X] [TopologicalSpace Y]7879theorem subset_seqClosure {s : Set X} : s ⊆ seqClosure s := fun p hp =>80 ⟨const ℕ p, fun _ => hp, tendsto_const_nhds⟩8182/-- The sequential closure of a set is contained in the closure of that set.83The converse is not true. -/84theorem seqClosure_subset_closure {s : Set X} : seqClosure s ⊆ closure s := fun _p ⟨_x, xM, xp⟩ =>85 mem_closure_of_tendsto xp (univ_mem' xM)8687/-- The sequential closure of a sequentially closed set is the set itself. -/88theorem IsSeqClosed.seqClosure_eq {s : Set X} (hs : IsSeqClosed s) : seqClosure s = s :=89 Subset.antisymm (fun _p ⟨_x, hx, hp⟩ => hs hx hp) subset_seqClosure9091/-- If a set is equal to its sequential closure, then it is sequentially closed. -/92theorem isSeqClosed_of_seqClosure_eq {s : Set X} (hs : seqClosure s = s) : IsSeqClosed s :=93 fun x _p hxs hxp => hs ▸ ⟨x, hxs, hxp⟩9495/-- A set is sequentially closed iff it is equal to its sequential closure. -/96theorem isSeqClosed_iff {s : Set X} : IsSeqClosed s ↔ seqClosure s = s :=97 ⟨IsSeqClosed.seqClosure_eq, isSeqClosed_of_seqClosure_eq⟩9899/-- A set is sequentially closed if it is closed. -/100protected theorem IsClosed.isSeqClosed {s : Set X} (hc : IsClosed s) : IsSeqClosed s :=101 fun _u _x hu hx => hc.mem_of_tendsto hx (Eventually.of_forall hu)102103theorem seqClosure_eq_closure [FrechetUrysohnSpace X] (s : Set X) : seqClosure s = closure s :=104 seqClosure_subset_closure.antisymm <| FrechetUrysohnSpace.closure_subset_seqClosure s105106/-- In a Fréchet-Urysohn space, a point belongs to the closure of a set iff it is a limit107of a sequence taking values in this set. -/108theorem mem_closure_iff_seq_limit [FrechetUrysohnSpace X] {s : Set X} {a : X} :109 a ∈ closure s ↔ ∃ x : ℕ → X, (∀ n : ℕ, x n ∈ s) ∧ Tendsto x atTop (𝓝 a) := by110 rw [← seqClosure_eq_closure]111 rfl112113/-- If the domain of a function `f : α → β` is a Fréchet-Urysohn space, then convergence114is equivalent to sequential convergence. See also `Filter.tendsto_iff_seq_tendsto` for a version115that works for any pair of filters assuming that the filter in the domain is countably generated.116117This property is equivalent to the definition of `FrechetUrysohnSpace`, see118`FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto`. -/119theorem tendsto_nhds_iff_seq_tendsto [FrechetUrysohnSpace X] {f : X → Y} {a : X} {b : Y} :120 Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ u : ℕ → X, Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b) := by121 refine122 ⟨fun hf u hu => hf.comp hu, fun h =>123 ((nhds_basis_closeds _).tendsto_iff (nhds_basis_closeds _)).2 ?_⟩124 rintro s ⟨hbs, hsc⟩125 refine ⟨closure (f ⁻¹' s), ⟨mt ?_ hbs, isClosed_closure⟩, fun x => mt fun hx => subset_closure hx⟩126 rw [← seqClosure_eq_closure]127 rintro ⟨u, hus, hu⟩128 exact hsc.mem_of_tendsto (h u hu) (Eventually.of_forall hus)129130/-- An alternative construction for `FrechetUrysohnSpace`: if sequential convergence implies131convergence, then the space is a Fréchet-Urysohn space. -/132theorem FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto133 (h : ∀ (f : X → Prop) (a : X),134 (∀ u : ℕ → X, Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a) :135 FrechetUrysohnSpace X := by136 refine ⟨fun s x hcx => ?_⟩137 by_cases hx : x ∈ s138 · exact subset_seqClosure hx139 · obtain ⟨u, hux, hus⟩ : ∃ u : ℕ → X, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ x in atTop, u x ∈ s := by140 simpa only [ContinuousAt, hx, tendsto_nhds_true, (· ∘ ·), ← not_frequently, exists_prop,141 ← mem_closure_iff_frequently, hcx, imp_false, not_forall, not_not, not_false_eq_true,142 not_true_eq_false] using h (· ∉ s) x143 rcases extraction_of_frequently_atTop hus with ⟨φ, φ_mono, hφ⟩144 exact ⟨u ∘ φ, hφ, hux.comp φ_mono.tendsto_atTop⟩145146-- see Note [lower instance priority]147/-- Every first-countable space is a Fréchet-Urysohn space. -/148instance (priority := 100) FirstCountableTopology.frechetUrysohnSpace149 [FirstCountableTopology X] : FrechetUrysohnSpace X :=150 FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto fun _ _ => tendsto_iff_seq_tendsto.2151152-- see Note [lower instance priority]153/-- Every Fréchet-Urysohn space is a sequential space. -/154instance (priority := 100) FrechetUrysohnSpace.to_sequentialSpace [FrechetUrysohnSpace X] :155 SequentialSpace X :=156 ⟨fun s hs => by rw [← closure_eq_iff_isClosed, ← seqClosure_eq_closure, hs.seqClosure_eq]⟩157158theorem Topology.IsInducing.frechetUrysohnSpace [FrechetUrysohnSpace Y] {f : X → Y}159 (hf : IsInducing f) : FrechetUrysohnSpace X := by160 refine ⟨fun s x hx ↦ ?_⟩161 rw [hf.closure_eq_preimage_closure_image, mem_preimage, mem_closure_iff_seq_limit] at hx162 rcases hx with ⟨u, hus, hu⟩163 choose v hv hvu using hus164 refine ⟨v, hv, ?_⟩165 simpa only [hf.tendsto_nhds_iff, Function.comp_def, hvu]166167/-- Subtype of a Fréchet-Urysohn space is a Fréchet-Urysohn space. -/168instance Subtype.instFrechetUrysohnSpace [FrechetUrysohnSpace X] {p : X → Prop} :169 FrechetUrysohnSpace (Subtype p) :=170 IsInducing.subtypeVal.frechetUrysohnSpace171172/-- In a sequential space, a set is closed iff it's sequentially closed. -/173theorem isSeqClosed_iff_isClosed [SequentialSpace X] {M : Set X} : IsSeqClosed M ↔ IsClosed M :=174 ⟨IsSeqClosed.isClosed, IsClosed.isSeqClosed⟩175176/-- If `x : ℕ → X` has no convergent subsequence, then `⋃ i, closure {x i}` is closed. -/177lemma isClosed_iUnion_closure_singleton_of_not_tendsto {x : ℕ → X} [SequentialSpace X]178 (hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)) :179 IsClosed (⋃ i, closure {x i}) := by180 refine IsSeqClosed.isClosed fun y l hy hy' => ?_181 by_cases! hm : ∃ m, ∃ᶠ n in atTop, y n ∈ closure {x m}182 · obtain ⟨m, pm⟩ := hm183 exact subset_iUnion _ m (isClosed_closure.mem_of_frequently_of_tendsto pm hy')184 · have (j : ℕ) : ∃ᶠ k in atTop, ∃ n ≥ j, y n ∈ closure {x k} := by185 refine frequently_atTop.2 fun a => ?_186 have := (Filter.eventually_all_finite (by simp : (Iic a).Finite)).2 fun i hi => hm i187 simp only [mem_Iic, eventually_atTop] at this188 obtain ⟨c, hc⟩ := this189 obtain ⟨b, hb⟩ := mem_iUnion.1 (hy (c + j))190 refine ⟨b, ?_, c + j, j.le_add_left c, hb⟩191 by_contra! hab192 simp_all [hc (c + j) (c.le_add_right j) b hab.le]193 obtain ⟨φ, hφ⟩ := extraction_forall_of_frequently this194 choose ψ hψ1 hψ2 using hφ.2195 have : Tendsto ψ atTop atTop := tendsto_atTop_mono hψ1 tendsto_id196 refine (hx l φ hφ.1 (Tendsto.specializes (hy'.comp this) (fun n => ?_))).elim197 exact specializes_iff_mem_closure.2 (hψ2 n)198199/-- If `x : ℕ → X` has no convergent subsequence in a T₁ sequential space, then its range is200closed. -/201lemma isClosed_range_of_not_tendsto {x : ℕ → X} [SequentialSpace X] [T1Space X]202 (hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)) :203 IsClosed (range x) := by204 simpa using isClosed_iUnion_closure_singleton_of_not_tendsto hx205206/-- The preimage of a sequentially closed set under a sequentially continuous map is sequentially207closed. -/208theorem IsSeqClosed.preimage {f : X → Y} {s : Set Y} (hs : IsSeqClosed s) (hf : SeqContinuous f) :209 IsSeqClosed (f ⁻¹' s) := fun _x _p hx hp => hs hx (hf hp)210211-- A continuous function is sequentially continuous.212protected theorem Continuous.seqContinuous {f : X → Y} (hf : Continuous f) : SeqContinuous f :=213 fun _x p hx => (hf.tendsto p).comp hx214215/-- A sequentially continuous function defined on a sequential space is continuous. -/216protected theorem SeqContinuous.continuous [SequentialSpace X] {f : X → Y} (hf : SeqContinuous f) :217 Continuous f :=218 continuous_iff_isClosed.mpr fun _s hs => (hs.isSeqClosed.preimage hf).isClosed219220/-- If the domain of a function is a sequential space, then continuity of this function is221equivalent to its sequential continuity. -/222theorem continuous_iff_seqContinuous [SequentialSpace X] {f : X → Y} :223 Continuous f ↔ SeqContinuous f :=224 ⟨Continuous.seqContinuous, SeqContinuous.continuous⟩225226theorem SequentialSpace.coinduced [SequentialSpace X] {Y} (f : X → Y) :227 @SequentialSpace Y (.coinduced f ‹_›) :=228 letI : TopologicalSpace Y := .coinduced f ‹_›229 ⟨fun _ hs ↦ isClosed_coinduced.2 (hs.preimage continuous_coinduced_rng.seqContinuous).isClosed⟩230231protected theorem SequentialSpace.iSup {X} {ι : Sort*} {t : ι → TopologicalSpace X}232 (h : ∀ i, @SequentialSpace X (t i)) : @SequentialSpace X (⨆ i, t i) := by233 letI : TopologicalSpace X := ⨆ i, t i234 refine ⟨fun s hs ↦ isClosed_iSup_iff.2 fun i ↦ ?_⟩235 letI := t i236 exact IsSeqClosed.isClosed fun u x hus hux ↦ hs hus <| hux.mono_right <| nhds_mono <| le_iSup _ _237238protected theorem SequentialSpace.sup {X} {t₁ t₂ : TopologicalSpace X}239 (h₁ : @SequentialSpace X t₁) (h₂ : @SequentialSpace X t₂) :240 @SequentialSpace X (t₁ ⊔ t₂) := by241 rw [sup_eq_iSup]242 exact .iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩243244lemma Topology.IsQuotientMap.sequentialSpace [SequentialSpace X] {f : X → Y}245 (hf : IsQuotientMap f) : SequentialSpace Y := hf.isCoinducing.eq_coinduced.symm ▸ .coinduced f246247/-- The quotient of a sequential space is a sequential space. -/248instance Quotient.instSequentialSpace [SequentialSpace X] {s : Setoid X} :249 SequentialSpace (Quotient s) :=250 isQuotientMap_quot_mk.sequentialSpace251252/-- The sum (disjoint union) of two sequential spaces is a sequential space. -/253instance Sum.instSequentialSpace [SequentialSpace X] [SequentialSpace Y] :254 SequentialSpace (X ⊕ Y) :=255 .sup (.coinduced Sum.inl) (.coinduced Sum.inr)256257/-- The disjoint union of an indexed family of sequential spaces is a sequential space. -/258instance Sigma.instSequentialSpace {ι : Type*} {X : ι → Type*}259 [∀ i, TopologicalSpace (X i)] [∀ i, SequentialSpace (X i)] : SequentialSpace (Σ i, X i) :=260 .iSup fun _ ↦ .coinduced _261262end TopologicalSpace263264section SeqCompact265266open TopologicalSpace FirstCountableTopology267268variable [TopologicalSpace X]269270theorem IsSeqCompact.subseq_of_frequently_in {s : Set X} (hs : IsSeqCompact s) {x : ℕ → X}271 (hx : ∃ᶠ n in atTop, x n ∈ s) :272 ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) :=273 let ⟨ψ, hψ, huψ⟩ := extraction_of_frequently_atTop hx274 let ⟨a, a_in, φ, hφ, h⟩ := hs huψ275 ⟨a, a_in, ψ ∘ φ, hψ.comp hφ, h⟩276277theorem SeqCompactSpace.tendsto_subseq [SeqCompactSpace X] (x : ℕ → X) :278 ∃ (a : X) (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) :=279 let ⟨a, _, φ, mono, h⟩ := isSeqCompact_univ fun n => mem_univ (x n)280 ⟨a, φ, mono, h⟩281282section FirstCountableTopology283284variable [FirstCountableTopology X]285286open FirstCountableTopology287288protected theorem IsCompact.isSeqCompact {s : Set X} (hs : IsCompact s) : IsSeqCompact s :=289 fun _x x_in =>290 let ⟨a, a_in, ha⟩ := hs (tendsto_principal.mpr (Eventually.of_forall x_in))291 ⟨a, a_in, MapClusterPt.tendsto_subseq ha⟩292293theorem IsCompact.tendsto_subseq' {s : Set X} {x : ℕ → X} (hs : IsCompact s)294 (hx : ∃ᶠ n in atTop, x n ∈ s) :295 ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) :=296 hs.isSeqCompact.subseq_of_frequently_in hx297298theorem IsCompact.tendsto_subseq {s : Set X} {x : ℕ → X} (hs : IsCompact s) (hx : ∀ n, x n ∈ s) :299 ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) :=300 hs.isSeqCompact hx301302-- see Note [lower instance priority]303instance (priority := 100) FirstCountableTopology.seq_compact_of_compact [CompactSpace X] :304 SeqCompactSpace X :=305 ⟨isCompact_univ.isSeqCompact⟩306307theorem CompactSpace.tendsto_subseq [CompactSpace X] (x : ℕ → X) :308 ∃ (a : _) (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) :=309 SeqCompactSpace.tendsto_subseq x310311end FirstCountableTopology312313section Image314315variable [TopologicalSpace Y] {f : X → Y}316317/-- Sequential compactness of sets is preserved under sequentially continuous functions. -/318theorem IsSeqCompact.image (f_cont : SeqContinuous f) {K : Set X} (K_cpt : IsSeqCompact K) :319 IsSeqCompact (f '' K) := by320 intro ys ys_in_fK321 choose xs xs_in_K fxs_eq_ys using ys_in_fK322 obtain ⟨a, a_in_K, phi, phi_mono, xs_phi_lim⟩ := K_cpt xs_in_K323 refine ⟨f a, mem_image_of_mem f a_in_K, phi, phi_mono, ?_⟩324 exact (f_cont xs_phi_lim).congr fun x ↦ fxs_eq_ys (phi x)325326/-- The range of sequentially continuous function on a sequentially compact space is sequentially327compact. -/328theorem IsSeqCompact.range [SeqCompactSpace X] (f_cont : SeqContinuous f) :329 IsSeqCompact (Set.range f) := by330 simpa using isSeqCompact_univ.image f_cont331332end Image333334end SeqCompact335336section UniformSpaceSeqCompact337338open uniformity339340open UniformSpace Prod341342variable [UniformSpace X] {s : Set X}343344theorem IsSeqCompact.exists_tendsto_of_frequently_mem (hs : IsSeqCompact s) {u : ℕ → X}345 (hu : ∃ᶠ n in atTop, u n ∈ s) (huc : CauchySeq u) : ∃ x ∈ s, Tendsto u atTop (𝓝 x) :=346 let ⟨x, hxs, _φ, φ_mono, hx⟩ := hs.subseq_of_frequently_in hu347 ⟨x, hxs, tendsto_nhds_of_cauchySeq_of_subseq huc φ_mono.tendsto_atTop hx⟩348349theorem IsSeqCompact.exists_tendsto (hs : IsSeqCompact s) {u : ℕ → X} (hu : ∀ n, u n ∈ s)350 (huc : CauchySeq u) : ∃ x ∈ s, Tendsto u atTop (𝓝 x) :=351 hs.exists_tendsto_of_frequently_mem (Frequently.of_forall hu) huc352353/-- A sequentially compact set in a uniform space is totally bounded. -/354protected theorem IsSeqCompact.totallyBounded (h : IsSeqCompact s) : TotallyBounded s := by355 intro V V_in356 unfold IsSeqCompact at h357 contrapose! h358 obtain ⟨u, u_in, hu⟩ : ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ ∀ n m, m < n → u m ∉ ball (u n) V := by359 simp only [not_subset, mem_iUnion₂, not_exists, exists_prop] at h360 simpa only [forall_and, forall_mem_image, not_and] using! seq_of_forall_finite_exists h361 refine ⟨u, u_in, fun x _ φ hφ huφ => ?_⟩362 obtain ⟨N, hN⟩ : ∃ N, ∀ p q, p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V :=363 huφ.cauchySeq.mem_entourage V_in364 exact hu (φ <| N + 1) (φ N) (hφ <| Nat.lt_add_one N) (hN (N + 1) N N.le_succ le_rfl)365366variable [IsCountablyGenerated (𝓤 X)]367368/-- A sequentially compact set in a uniform space with countably generated uniformity filter369is complete. -/370protected theorem IsSeqCompact.isComplete (hs : IsSeqCompact s) : IsComplete s := fun l hl hls => by371 have := hl.1372 rcases exists_antitone_basis (𝓤 X) with ⟨V, hV⟩373 choose W hW hWV using fun n => comp_mem_uniformity_sets (hV.mem n)374 have hWV' : ∀ n, W n ⊆ V n := fun n ⟨x, y⟩ hx =>375 @hWV n (x, y) ⟨x, refl_mem_uniformity <| hW _, hx⟩376 obtain ⟨t, ht_anti, htl, htW, hts⟩ :377 ∃ t : ℕ → Set X, Antitone t ∧ (∀ n, t n ∈ l) ∧ (∀ n, t n ×ˢ t n ⊆ W n) ∧ ∀ n, t n ⊆ s := by378 have : ∀ n, ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s := by379 rw [le_principal_iff] at hls380 have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)381 simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff,382 prod_self_subset_prod_self, and_assoc] using! this383 choose t htl htW hts using this384 have : ∀ n : ℕ, ⋂ k ≤ n, t k ⊆ t n := fun n => by apply iInter₂_subset; rfl385 exact ⟨fun n => ⋂ k ≤ n, t k, fun m n h =>386 biInter_subset_biInter_left fun k (hk : k ≤ m) => hk.trans h, fun n =>387 (biInter_mem (finite_le_nat n)).2 fun k _ => htl k, fun n =>388 (prod_mono (this n) (this n)).trans (htW n), fun n => (this n).trans (hts n)⟩389 choose u hu using fun n => Filter.nonempty_of_mem (htl n)390 have huc : CauchySeq u := hV.toHasBasis.cauchySeq_iff.2 fun N _ =>391 ⟨N, fun m hm n hn => hWV' _ <| @htW N (_, _) ⟨ht_anti hm (hu _), ht_anti hn (hu _)⟩⟩392 rcases hs.exists_tendsto (fun n => hts n (hu n)) huc with ⟨x, hxs, hx⟩393 refine ⟨x, hxs, (nhds_basis_uniformity' hV.toHasBasis).ge_iff.2 fun N _ => ?_⟩394 obtain ⟨n, hNn, hn⟩ : ∃ n, N ≤ n ∧ u n ∈ ball x (W N) :=395 ((eventually_ge_atTop N).and (hx <| ball_mem_nhds x (hW N))).exists396 refine mem_of_superset (htl n) fun y hy => hWV N ⟨u n, hn, htW N ?_⟩397 exact ⟨ht_anti hNn (hu n), ht_anti hNn hy⟩398399end UniformSpaceSeqCompact400401section MetrizableSpaceSeqCompact402403variable [TopologicalSpace X] [PseudoMetrizableSpace X] {s : Set X}404405/-- In a (pseudo)metrizable space, any sequentially compact set is compact. -/406protected theorem IsSeqCompact.isCompact (hs : IsSeqCompact s) : IsCompact s :=407 letI := pseudoMetrizableSpaceUniformity X408 haveI := pseudoMetrizableSpaceUniformity_countably_generated X409 isCompact_iff_totallyBounded_isComplete.2 ⟨hs.totallyBounded, hs.isComplete⟩410411/-- A version of **Bolzano-Weierstrass**: in a (pseudo)metrizable space, a set is compact if and412only if it is sequentially compact. -/413theorem isCompact_iff_isSeqCompact : IsCompact s ↔ IsSeqCompact s :=414 ⟨fun H => H.isSeqCompact, fun H => H.isCompact⟩415416@[deprecated (since := "2025-12-23")]417protected alias UniformSpace.isCompact_iff_isSeqCompact := isCompact_iff_isSeqCompact418419theorem compactSpace_iff_seqCompactSpace : CompactSpace X ↔ SeqCompactSpace X := by420 simp only [← isCompact_univ_iff, seqCompactSpace_iff, isCompact_iff_isSeqCompact]421422@[deprecated (since := "2025-12-23")]423protected alias UniformSpace.compactSpace_iff_seqCompactSpace := compactSpace_iff_seqCompactSpace424425end MetrizableSpaceSeqCompact