doc-next-gen

Mathlib.Topology.Sequences

Module docstring

{"# Sequences in topological spaces

In this file we prove theorems about relations between closure/compactness/continuity etc and their sequential counterparts.

Main definitions

The following notions are defined in Topology/Defs/Sequences. We build theory about these definitions here, so we remind the definitions.

Set operation

  • seqClosure s: sequential closure of a set, the set of limits of sequences of points of s;

Predicates

  • IsSeqClosed s: predicate saying that a set is sequentially closed, i.e., seqClosure s ⊆ s;
  • SeqContinuous f: predicate saying that a function is sequentially continuous, i.e., for any sequence u : ℕ → X that converges to a point x, the sequence f ∘ u converges to f x;
  • IsSeqCompact s: predicate saying that a set is sequentially compact, i.e., every sequence taking values in s has a converging subsequence.

Type classes

  • FrechetUrysohnSpace X: a typeclass saying that a topological space is a Fréchet-Urysohn space, i.e., the sequential closure of any set is equal to its closure.
  • SequentialSpace X: a typeclass saying that a topological space is a sequential space, i.e., any sequentially closed set in this space is closed. This condition is weaker than being a Fréchet-Urysohn space.
  • SeqCompactSpace X: a typeclass saying that a topological space is sequentially compact, i.e., every sequence in X has a converging subsequence.

Main results

  • seqClosure_subset_closure: closure of a set includes its sequential closure;
  • IsClosed.isSeqClosed: a closed set is sequentially closed;
  • IsSeqClosed.seqClosure_eq: sequential closure of a sequentially closed set s is equal to s;
  • seqClosure_eq_closure: in a Fréchet-Urysohn space, the sequential closure of a set is equal to its closure;
  • tendsto_nhds_iff_seq_tendsto, FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto: a topological space is a Fréchet-Urysohn space if and only if sequential convergence implies convergence;
  • FirstCountableTopology.frechetUrysohnSpace: every topological space with first countable topology is a Fréchet-Urysohn space;
  • FrechetUrysohnSpace.to_sequentialSpace: every Fréchet-Urysohn space is a sequential space;
  • IsSeqCompact.isCompact: a sequentially compact set in a uniform space with countably generated uniformity is compact.

Tags

sequentially closed, sequentially compact, sequential space ","### Sequential closures, sequential continuity, and sequential spaces. "}

seqClosure_subset_closure theorem
{s : Set X} : seqClosure s ⊆ closure s
Full source 
/-- The sequential closure of a set is contained in the closure of that set.
The converse is not true. -/
theorem seqClosure_subset_closure {s : Set X} : seqClosureseqClosure s ⊆ closure s := fun _p ⟨_x, xM, xp⟩ =>
  mem_closure_of_tendsto xp (univ_mem' xM)
Sequential Closure is Subset of Topological Closure
Informal description
For any subset $s$ of a topological space $X$, the sequential closure of $s$ is contained in the topological closure of $s$. That is, every limit point of a sequence in $s$ is also a limit point of $s$ in the topological sense.
IsSeqClosed.seqClosure_eq theorem
{s : Set X} (hs : IsSeqClosed s) : seqClosure s = s
Full source 
/-- The sequential closure of a sequentially closed set is the set itself. -/
theorem IsSeqClosed.seqClosure_eq {s : Set X} (hs : IsSeqClosed s) : seqClosure s = s :=
  Subset.antisymm (fun _p ⟨_x, hx, hp⟩ => hs hx hp) subset_seqClosure
Sequential Closure of a Sequentially Closed Set Equals Itself
Informal description
For any subset $s$ of a topological space $X$, if $s$ is sequentially closed (i.e., contains all limits of sequences of its points), then the sequential closure of $s$ is equal to $s$ itself, i.e., $\text{seqClosure}(s) = s$.
isSeqClosed_of_seqClosure_eq theorem
{s : Set X} (hs : seqClosure s = s) : IsSeqClosed s
Full source 
/-- If a set is equal to its sequential closure, then it is sequentially closed. -/
theorem isSeqClosed_of_seqClosure_eq {s : Set X} (hs : seqClosure s = s) : IsSeqClosed s :=
  fun x _p hxs hxp => hs ▸ ⟨x, hxs, hxp⟩
Sequential Closure Equality Implies Sequential Closedness
Informal description
For any subset $s$ of a topological space $X$, if the sequential closure of $s$ is equal to $s$ itself, then $s$ is sequentially closed. That is, if $\text{seqClosure}(s) = s$, then $s$ contains all limits of sequences of points in $s$.
isSeqClosed_iff theorem
{s : Set X} : IsSeqClosed s ↔ seqClosure s = s
Full source 
/-- A set is sequentially closed iff it is equal to its sequential closure. -/
theorem isSeqClosed_iff {s : Set X} : IsSeqClosedIsSeqClosed s ↔ seqClosure s = s :=
  ⟨IsSeqClosed.seqClosure_eq, isSeqClosed_of_seqClosure_eq⟩
Characterization of Sequentially Closed Sets via Sequential Closure
Informal description
A subset $s$ of a topological space $X$ is sequentially closed if and only if its sequential closure $\text{seqClosure}(s)$ is equal to $s$. That is, $s$ contains all limits of sequences of its points if and only if $\text{seqClosure}(s) = s$.
IsClosed.isSeqClosed theorem
{s : Set X} (hc : IsClosed s) : IsSeqClosed s
Full source 
/-- A set is sequentially closed if it is closed. -/
protected theorem IsClosed.isSeqClosed {s : Set X} (hc : IsClosed s) : IsSeqClosed s :=
  fun _u _x hu hx => hc.mem_of_tendsto hx (Eventually.of_forall hu)
Closed Sets are Sequentially Closed
Informal description
For any closed subset $s$ of a topological space $X$, $s$ is sequentially closed, meaning that the sequential closure of $s$ is contained in $s$.
seqClosure_eq_closure theorem
[FrechetUrysohnSpace X] (s : Set X) : seqClosure s = closure s
Full source 
theorem seqClosure_eq_closure [FrechetUrysohnSpace X] (s : Set X) : seqClosure s = closure s :=
  seqClosure_subset_closure.antisymm <| FrechetUrysohnSpace.closure_subset_seqClosure s
Sequential Closure Equals Topological Closure in Fréchet-Urysohn Spaces
Informal description
In a Fréchet-Urysohn space $X$, the sequential closure of any subset $s$ is equal to its topological closure, i.e., $\text{seqClosure}(s) = \overline{s}$.
mem_closure_iff_seq_limit theorem
[FrechetUrysohnSpace X] {s : Set X} {a : X} : a ∈ closure s ↔ ∃ x : ℕ → X, (∀ n : ℕ, x n ∈ s) ∧ Tendsto x atTop (𝓝 a)
Full source 
/-- In a Fréchet-Urysohn space, a point belongs to the closure of a set iff it is a limit
of a sequence taking values in this set. -/
theorem mem_closure_iff_seq_limit [FrechetUrysohnSpace X] {s : Set X} {a : X} :
    a ∈ closure sa ∈ closure s ↔ ∃ x : ℕ → X, (∀ n : ℕ, x n ∈ s) ∧ Tendsto x atTop (𝓝 a) := by
  rw [← seqClosure_eq_closure]
  rfl
Characterization of Closure via Sequences in Fréchet-Urysohn Spaces
Informal description
Let $X$ be a Fréchet-Urysohn space and $s \subseteq X$ a subset. A point $a \in X$ belongs to the closure of $s$ if and only if there exists a sequence $(x_n)_{n \in \mathbb{N}}$ in $s$ that converges to $a$.
tendsto_nhds_iff_seq_tendsto theorem
[FrechetUrysohnSpace X] {f : X → Y} {a : X} {b : Y} : Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ u : ℕ → X, Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
Full source 
/-- If the domain of a function `f : α → β` is a Fréchet-Urysohn space, then convergence
is equivalent to sequential convergence. See also `Filter.tendsto_iff_seq_tendsto` for a version
that works for any pair of filters assuming that the filter in the domain is countably generated.

This property is equivalent to the definition of `FrechetUrysohnSpace`, see
`FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto`. -/
theorem tendsto_nhds_iff_seq_tendsto [FrechetUrysohnSpace X] {f : X → Y} {a : X} {b : Y} :
    TendstoTendsto f (𝓝 a) (𝓝 b) ↔ ∀ u : ℕ → X, Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b) := by
  refine
    ⟨fun hf u hu => hf.comp hu, fun h =>
      ((nhds_basis_closeds _).tendsto_iff (nhds_basis_closeds _)).2 ?_⟩
  rintro s ⟨hbs, hsc⟩
  refine ⟨closure (f ⁻¹' s), ⟨mt ?_ hbs, isClosed_closure⟩, fun x => mt fun hx => subset_closure hx⟩
  rw [← seqClosure_eq_closure]
  rintro ⟨u, hus, hu⟩
  exact hsc.mem_of_tendsto (h u hu) (Eventually.of_forall hus)
Characterization of Convergence via Sequences in Fréchet-Urysohn Spaces
Informal description
Let $X$ be a Fréchet-Urysohn space and $Y$ a topological space. For a function $f : X \to Y$ and points $a \in X$, $b \in Y$, the following are equivalent: 1. $f$ tends to $b$ as $x$ approaches $a$ (i.e., $\lim_{x \to a} f(x) = b$) 2. For every sequence $(u_n)_{n \in \mathbb{N}}$ in $X$ converging to $a$, the sequence $(f(u_n))_{n \in \mathbb{N}}$ converges to $b$.
FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto theorem
(h : ∀ (f : X → Prop) (a : X), (∀ u : ℕ → X, Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a) : FrechetUrysohnSpace X
Full source 
/-- An alternative construction for `FrechetUrysohnSpace`: if sequential convergence implies
convergence, then the space is a Fréchet-Urysohn space. -/
theorem FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto
    (h : ∀ (f : X → Prop) (a : X),
      (∀ u : ℕ → X, Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a) :
    FrechetUrysohnSpace X := by
  refine ⟨fun s x hcx => ?_⟩
  by_cases hx : x ∈ s
  · exact subset_seqClosure hx
  · obtain ⟨u, hux, hus⟩ : ∃ u : ℕ → X, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ x in atTop, u x ∈ s := by
      simpa only [ContinuousAt, hx, tendsto_nhds_true, (· ∘ ·), ← not_frequently, exists_prop,
        ← mem_closure_iff_frequently, hcx, imp_false, not_forall, not_not, not_false_eq_true,
        not_true_eq_false] using h (· ∉ s) x
    rcases extraction_of_frequently_atTop hus with ⟨φ, φ_mono, hφ⟩
    exact ⟨u ∘ φ, hφ, hux.comp φ_mono.tendsto_atTop⟩
Fréchet-Urysohn Space Characterization via Sequential Continuity
Informal description
A topological space $X$ is a Fréchet-Urysohn space if, for every function $f : X \to \text{Prop}$ and every point $a \in X$, the following holds: if for every sequence $u : \mathbb{N} \to X$ converging to $a$, the sequence $f \circ u$ converges to $f(a)$, then $f$ is continuous at $a$.
FirstCountableTopology.frechetUrysohnSpace instance
[FirstCountableTopology X] : FrechetUrysohnSpace X
Full source 
/-- Every first-countable space is a Fréchet-Urysohn space. -/
instance (priority := 100) FirstCountableTopology.frechetUrysohnSpace
    [FirstCountableTopology X] : FrechetUrysohnSpace X :=
  FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto fun _ _ => tendsto_iff_seq_tendsto.2
First-Countable Spaces are Fréchet-Urysohn Spaces
Informal description
Every first-countable topological space is a Fréchet-Urysohn space.
Topology.IsInducing.frechetUrysohnSpace theorem
[FrechetUrysohnSpace Y] {f : X → Y} (hf : IsInducing f) : FrechetUrysohnSpace X
Full source 
theorem Topology.IsInducing.frechetUrysohnSpace [FrechetUrysohnSpace Y] {f : X → Y}
    (hf : IsInducing f) : FrechetUrysohnSpace X := by
  refine ⟨fun s x hx ↦ ?_⟩
  rw [hf.closure_eq_preimage_closure_image, mem_preimage, mem_closure_iff_seq_limit] at hx
  rcases hx with ⟨u, hus, hu⟩
  choose v hv hvu using hus
  refine ⟨v, hv, ?_⟩
  simpa only [hf.tendsto_nhds_iff, Function.comp_def, hvu]
Induced Fréchet-Urysohn Property via Inducing Maps
Informal description
Let $Y$ be a Fréchet-Urysohn space and $f : X \to Y$ an inducing map between topological spaces. Then $X$ is also a Fréchet-Urysohn space.
Subtype.instFrechetUrysohnSpace instance
[FrechetUrysohnSpace X] {p : X → Prop} : FrechetUrysohnSpace (Subtype p)
Full source 
/-- Subtype of a Fréchet-Urysohn space is a Fréchet-Urysohn space. -/
instance Subtype.instFrechetUrysohnSpace [FrechetUrysohnSpace X] {p : X → Prop} :
    FrechetUrysohnSpace (Subtype p) :=
  IsInducing.subtypeVal.frechetUrysohnSpace
Subtypes of Fréchet-Urysohn Spaces are Fréchet-Urysohn
Informal description
For any Fréchet-Urysohn space $X$ and any predicate $p$ on $X$, the subtype $\{x \in X \mid p(x)\}$ is also a Fréchet-Urysohn space.
isSeqClosed_iff_isClosed theorem
[SequentialSpace X] {M : Set X} : IsSeqClosed M ↔ IsClosed M
Full source 
/-- In a sequential space, a set is closed iff it's sequentially closed. -/
theorem isSeqClosed_iff_isClosed [SequentialSpace X] {M : Set X} : IsSeqClosedIsSeqClosed M ↔ IsClosed M :=
  ⟨IsSeqClosed.isClosed, IsClosed.isSeqClosed⟩
Sequential Closedness Equivalence in Sequential Spaces
Informal description
In a sequential space $X$, a subset $M \subseteq X$ is sequentially closed if and only if it is closed. That is, $M$ contains all its sequential limits precisely when $M$ is closed in the topology of $X$.
IsSeqClosed.preimage theorem
{f : X → Y} {s : Set Y} (hs : IsSeqClosed s) (hf : SeqContinuous f) : IsSeqClosed (f ⁻¹' s)
Full source 
/-- The preimage of a sequentially closed set under a sequentially continuous map is sequentially
closed. -/
theorem IsSeqClosed.preimage {f : X → Y} {s : Set Y} (hs : IsSeqClosed s) (hf : SeqContinuous f) :
    IsSeqClosed (f ⁻¹' s) := fun _x _p hx hp => hs hx (hf hp)
Preimage of a Sequentially Closed Set under a Sequentially Continuous Function is Sequentially Closed
Informal description
Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ be a sequentially continuous function, and $s \subseteq Y$ be a sequentially closed set. Then the preimage $f^{-1}(s)$ is sequentially closed in $X$.
Continuous.seqContinuous theorem
{f : X → Y} (hf : Continuous f) : SeqContinuous f
Full source 
protected theorem Continuous.seqContinuous {f : X → Y} (hf : Continuous f) : SeqContinuous f :=
  fun _x p hx => (hf.tendsto p).comp hx
Continuous Functions are Sequentially Continuous
Informal description
Let $X$ and $Y$ be topological spaces. If a function $f \colon X \to Y$ is continuous, then it is sequentially continuous, meaning that for any sequence $(x_n)$ in $X$ converging to a point $x \in X$, the sequence $(f(x_n))$ converges to $f(x)$ in $Y$.
SeqContinuous.continuous theorem
[SequentialSpace X] {f : X → Y} (hf : SeqContinuous f) : Continuous f
Full source 
/-- A sequentially continuous function defined on a sequential space is continuous. -/
protected theorem SeqContinuous.continuous [SequentialSpace X] {f : X → Y} (hf : SeqContinuous f) :
    Continuous f :=
  continuous_iff_isClosed.mpr fun _s hs => (hs.isSeqClosed.preimage hf).isClosed
Sequential Continuity Implies Continuity on Sequential Spaces
Informal description
Let $X$ be a sequential topological space and $Y$ be any topological space. If a function $f \colon X \to Y$ is sequentially continuous, then it is continuous.
continuous_iff_seqContinuous theorem
[SequentialSpace X] {f : X → Y} : Continuous f ↔ SeqContinuous f
Full source 
/-- If the domain of a function is a sequential space, then continuity of this function is
equivalent to its sequential continuity. -/
theorem continuous_iff_seqContinuous [SequentialSpace X] {f : X → Y} :
    ContinuousContinuous f ↔ SeqContinuous f :=
  ⟨Continuous.seqContinuous, SeqContinuous.continuous⟩
Equivalence of Continuity and Sequential Continuity on Sequential Spaces
Informal description
Let $X$ be a sequential topological space and $Y$ be any topological space. For a function $f \colon X \to Y$, the following are equivalent: 1. $f$ is continuous. 2. $f$ is sequentially continuous, i.e., for any sequence $(x_n)$ in $X$ converging to a point $x \in X$, the sequence $(f(x_n))$ converges to $f(x)$ in $Y$.
SequentialSpace.coinduced theorem
[SequentialSpace X] {Y} (f : X → Y) : @SequentialSpace Y (.coinduced f ‹_›)
Full source 
theorem SequentialSpace.coinduced [SequentialSpace X] {Y} (f : X → Y) :
    @SequentialSpace Y (.coinduced f ‹_›) :=
  letI : TopologicalSpace Y := .coinduced f ‹_›
  ⟨fun _ hs ↦ isClosed_coinduced.2 (hs.preimage continuous_coinduced_rng.seqContinuous).isClosed⟩
Coinduced Topology Preserves Sequentiality
Informal description
Let $X$ be a sequential space and $f \colon X \to Y$ be a function. Then the topological space on $Y$ coinduced by $f$ is also sequential.
SequentialSpace.iSup theorem
{X} {ι : Sort*} {t : ι → TopologicalSpace X} (h : ∀ i, @SequentialSpace X (t i)) : @SequentialSpace X (⨆ i, t i)
Full source 
protected theorem SequentialSpace.iSup {X} {ι : Sort*} {t : ι → TopologicalSpace X}
    (h : ∀ i, @SequentialSpace X (t i)) : @SequentialSpace X (⨆ i, t i) := by
  letI : TopologicalSpace X := ⨆ i, t i
  refine ⟨fun s hs ↦ isClosed_iSup_iff.2 fun i ↦ ?_⟩
  letI := t i
  exact IsSeqClosed.isClosed fun u x hus hux ↦ hs hus <| hux.mono_right <| nhds_mono <| le_iSup _ _
Supremum of Sequential Topologies is Sequential
Informal description
Let $X$ be a topological space and $\{t_i\}_{i \in \iota}$ be a family of topologies on $X$ indexed by a type $\iota$. If for each $i \in \iota$, the topological space $(X, t_i)$ is sequential, then the supremum topology $\bigsqcup_{i \in \iota} t_i$ on $X$ is also sequential.
SequentialSpace.sup theorem
{X} {t₁ t₂ : TopologicalSpace X} (h₁ : @SequentialSpace X t₁) (h₂ : @SequentialSpace X t₂) : @SequentialSpace X (t₁ ⊔ t₂)
Full source 
protected theorem SequentialSpace.sup {X} {t₁ t₂ : TopologicalSpace X}
    (h₁ : @SequentialSpace X t₁) (h₂ : @SequentialSpace X t₂) :
    @SequentialSpace X (t₁ ⊔ t₂) := by
  rw [sup_eq_iSup]
  exact .iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩
Supremum of Two Sequential Topologies is Sequential
Informal description
Let $X$ be a topological space equipped with two topologies $t_1$ and $t_2$. If both $(X, t_1)$ and $(X, t_2)$ are sequential spaces, then the topological space $(X, t_1 \sqcup t_2)$ is also sequential, where $t_1 \sqcup t_2$ denotes the supremum of the two topologies.
Quotient.instSequentialSpace instance
[SequentialSpace X] {s : Setoid X} : SequentialSpace (Quotient s)
Full source 
/-- The quotient of a sequential space is a sequential space. -/
instance Quotient.instSequentialSpace [SequentialSpace X] {s : Setoid X} :
    SequentialSpace (Quotient s) :=
  isQuotientMap_quot_mk.sequentialSpace
Quotient of a Sequential Space is Sequential
Informal description
For any sequential space $X$ and equivalence relation $s$ on $X$, the quotient space $X/s$ is also a sequential space.
Sum.instSequentialSpace instance
[SequentialSpace X] [SequentialSpace Y] : SequentialSpace (X ⊕ Y)
Full source 
/-- The sum (disjoint union) of two sequential spaces is a sequential space. -/
instance Sum.instSequentialSpace [SequentialSpace X] [SequentialSpace Y] :
    SequentialSpace (X ⊕ Y) :=
  .sup (.coinduced Sum.inl) (.coinduced Sum.inr)
Disjoint Union of Sequential Spaces is Sequential
Informal description
The disjoint union $X \oplus Y$ of two sequential spaces $X$ and $Y$ is also a sequential space.
Sigma.instSequentialSpace instance
{ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, SequentialSpace (X i)] : SequentialSpace (Σ i, X i)
Full source 
/-- The disjoint union of an indexed family of sequential spaces is a sequential space. -/
instance Sigma.instSequentialSpace {ι : Type*} {X : ι → Type*}
    [∀ i, TopologicalSpace (X i)] [∀ i, SequentialSpace (X i)] : SequentialSpace (Σ i, X i) :=
  .iSup fun _ ↦ .coinduced _
Disjoint Union of Sequential Spaces is Sequential
Informal description
For any family of topological spaces $\{X_i\}_{i \in \iota}$ where each $X_i$ is a sequential space, the disjoint union $\Sigma i, X_i$ is also a sequential space.
IsSeqCompact.subseq_of_frequently_in theorem
{s : Set X} (hs : IsSeqCompact s) {x : ℕ → X} (hx : ∃ᶠ n in atTop, x n ∈ s) : ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
Full source 
theorem IsSeqCompact.subseq_of_frequently_in {s : Set X} (hs : IsSeqCompact s) {x : ℕ → X}
    (hx : ∃ᶠ n in atTop, x n ∈ s) :
    ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) :=
  let ⟨ψ, hψ, huψ⟩ := extraction_of_frequently_atTop hx
  let ⟨a, a_in, φ, hφ, h⟩ := hs huψ
  ⟨a, a_in, ψ ∘ φ, hψ.comp hφ, h⟩
Existence of Convergent Subsequence in Sequentially Compact Sets for Frequently Visiting Sequences
Informal description
Let $X$ be a topological space and $s \subseteq X$ be a sequentially compact set. If a sequence $x : \mathbb{N} \to X$ is frequently in $s$ (i.e., for any $N \in \mathbb{N}$, there exists $n \geq N$ such that $x_n \in s$), then there exists a point $a \in s$ and a strictly increasing function $\varphi : \mathbb{N} \to \mathbb{N}$ such that the subsequence $x \circ \varphi$ converges to $a$.
SeqCompactSpace.tendsto_subseq theorem
[SeqCompactSpace X] (x : ℕ → X) : ∃ (a : X) (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
Full source 
theorem SeqCompactSpace.tendsto_subseq [SeqCompactSpace X] (x : ℕ → X) :
    ∃ (a : X) (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) :=
  let ⟨a, _, φ, mono, h⟩ := isSeqCompact_univ fun n => mem_univ (x n)
  ⟨a, φ, mono, h⟩
Existence of Convergent Subsequence in Sequentially Compact Spaces
Informal description
In a sequentially compact topological space $X$, for any sequence $x \colon \mathbb{N} \to X$, there exists a point $a \in X$ and a strictly increasing function $\varphi \colon \mathbb{N} \to \mathbb{N}$ such that the subsequence $x \circ \varphi$ converges to $a$.
IsCompact.isSeqCompact theorem
{s : Set X} (hs : IsCompact s) : IsSeqCompact s
Full source 
protected theorem IsCompact.isSeqCompact {s : Set X} (hs : IsCompact s) : IsSeqCompact s :=
  fun _x x_in =>
  let ⟨a, a_in, ha⟩ := hs (tendsto_principal.mpr (Eventually.of_forall x_in))
  ⟨a, a_in, tendsto_subseq ha⟩
Compactness implies sequential compactness
Informal description
For any subset $s$ of a topological space $X$, if $s$ is compact, then it is sequentially compact. That is, every sequence in $s$ has a convergent subsequence with limit in $s$.
IsCompact.tendsto_subseq' theorem
{s : Set X} {x : ℕ → X} (hs : IsCompact s) (hx : ∃ᶠ n in atTop, x n ∈ s) : ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
Full source 
theorem IsCompact.tendsto_subseq' {s : Set X} {x : ℕ → X} (hs : IsCompact s)
    (hx : ∃ᶠ n in atTop, x n ∈ s) :
    ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) :=
  hs.isSeqCompact.subseq_of_frequently_in hx
Existence of Convergent Subsequence in Compact Sets for Frequently Visiting Sequences
Informal description
Let $X$ be a topological space and $s \subseteq X$ a compact subset. For any sequence $x \colon \mathbb{N} \to X$ that is frequently in $s$ (i.e., for every $N \in \mathbb{N}$, there exists $n \geq N$ such that $x_n \in s$), there exists a point $a \in s$ and a strictly increasing function $\varphi \colon \mathbb{N} \to \mathbb{N}$ such that the subsequence $x \circ \varphi$ converges to $a$.
IsCompact.tendsto_subseq theorem
{s : Set X} {x : ℕ → X} (hs : IsCompact s) (hx : ∀ n, x n ∈ s) : ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
Full source 
theorem IsCompact.tendsto_subseq {s : Set X} {x : ℕ → X} (hs : IsCompact s) (hx : ∀ n, x n ∈ s) :
    ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) :=
  hs.isSeqCompact hx
Existence of convergent subsequences in compact sets
Informal description
Let $X$ be a topological space and $s \subseteq X$ a compact subset. For any sequence $(x_n)_{n \in \mathbb{N}}$ in $s$, there exists a point $a \in s$ and a strictly increasing function $\varphi: \mathbb{N} \to \mathbb{N}$ such that the subsequence $(x_{\varphi(n)})_{n \in \mathbb{N}}$ converges to $a$.
CompactSpace.tendsto_subseq theorem
[CompactSpace X] (x : ℕ → X) : ∃ (a : _) (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
Full source 
theorem CompactSpace.tendsto_subseq [CompactSpace X] (x : ℕ → X) :
    ∃ (a : _) (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) :=
  SeqCompactSpace.tendsto_subseq x
Existence of Convergent Subsequence in Compact Spaces
Informal description
Let $X$ be a compact topological space. For any sequence $(x_n)_{n \in \mathbb{N}}$ in $X$, there exists a point $a \in X$ and a strictly increasing function $\varphi: \mathbb{N} \to \mathbb{N}$ such that the subsequence $(x_{\varphi(n)})_{n \in \mathbb{N}}$ converges to $a$.
IsSeqCompact.image theorem
(f_cont : SeqContinuous f) {K : Set X} (K_cpt : IsSeqCompact K) : IsSeqCompact (f '' K)
Full source 
/-- Sequential compactness of sets is preserved under sequentially continuous functions. -/
theorem IsSeqCompact.image (f_cont : SeqContinuous f) {K : Set X} (K_cpt : IsSeqCompact K) :
    IsSeqCompact (f '' K) := by
  intro ys ys_in_fK
  choose xs xs_in_K fxs_eq_ys using ys_in_fK
  obtain ⟨a, a_in_K, phi, phi_mono, xs_phi_lim⟩ := K_cpt xs_in_K
  refine ⟨f a, mem_image_of_mem f a_in_K, phi, phi_mono, ?_⟩
  exact (f_cont xs_phi_lim).congr fun x ↦ fxs_eq_ys (phi x)
Sequential Compactness is Preserved under Sequentially Continuous Images
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ be a sequentially continuous function, and $K \subseteq X$ be a sequentially compact set. Then the image $f(K)$ is sequentially compact in $Y$.
IsSeqCompact.range theorem
[SeqCompactSpace X] (f_cont : SeqContinuous f) : IsSeqCompact (Set.range f)
Full source 
/-- The range of sequentially continuous function on a sequentially compact space is sequentially
compact. -/
theorem IsSeqCompact.range [SeqCompactSpace X] (f_cont : SeqContinuous f) :
    IsSeqCompact (Set.range f) := by
  simpa using isSeqCompact_univ.image f_cont
Sequential Compactness of the Range of a Sequentially Continuous Function on a Sequentially Compact Space
Informal description
Let $X$ be a sequentially compact topological space and $Y$ be a topological space. If $f : X \to Y$ is a sequentially continuous function, then the range of $f$ is sequentially compact in $Y$.
IsSeqCompact.exists_tendsto_of_frequently_mem theorem
(hs : IsSeqCompact s) {u : ℕ → X} (hu : ∃ᶠ n in atTop, u n ∈ s) (huc : CauchySeq u) : ∃ x ∈ s, Tendsto u atTop (𝓝 x)
Full source 
theorem IsSeqCompact.exists_tendsto_of_frequently_mem (hs : IsSeqCompact s) {u : ℕ → X}
    (hu : ∃ᶠ n in atTop, u n ∈ s) (huc : CauchySeq u) : ∃ x ∈ s, Tendsto u atTop (𝓝 x) :=
  let ⟨x, hxs, _φ, φ_mono, hx⟩ := hs.subseq_of_frequently_in hu
  ⟨x, hxs, tendsto_nhds_of_cauchySeq_of_subseq huc φ_mono.tendsto_atTop hx⟩
Convergence of Frequently Visiting Cauchy Sequences in Sequentially Compact Sets
Informal description
Let $X$ be a topological space and $s \subseteq X$ be a sequentially compact set. If a sequence $u : \mathbb{N} \to X$ is frequently in $s$ (i.e., for any $N \in \mathbb{N}$, there exists $n \geq N$ such that $u_n \in s$) and $u$ is a Cauchy sequence, then there exists a point $x \in s$ such that $u$ converges to $x$.
IsSeqCompact.exists_tendsto theorem
(hs : IsSeqCompact s) {u : ℕ → X} (hu : ∀ n, u n ∈ s) (huc : CauchySeq u) : ∃ x ∈ s, Tendsto u atTop (𝓝 x)
Full source 
theorem IsSeqCompact.exists_tendsto (hs : IsSeqCompact s) {u : ℕ → X} (hu : ∀ n, u n ∈ s)
    (huc : CauchySeq u) : ∃ x ∈ s, Tendsto u atTop (𝓝 x) :=
  hs.exists_tendsto_of_frequently_mem (Frequently.of_forall hu) huc
Convergence of Cauchy Sequences in Sequentially Compact Sets
Informal description
Let $X$ be a topological space and $s \subseteq X$ be a sequentially compact set. If a sequence $u : \mathbb{N} \to X$ satisfies $u_n \in s$ for all $n \in \mathbb{N}$ and $u$ is a Cauchy sequence, then there exists a point $x \in s$ such that $u$ converges to $x$.
IsSeqCompact.totallyBounded theorem
(h : IsSeqCompact s) : TotallyBounded s
Full source 
/-- A sequentially compact set in a uniform space is totally bounded. -/
protected theorem IsSeqCompact.totallyBounded (h : IsSeqCompact s) : TotallyBounded s := by
  intro V V_in
  unfold IsSeqCompact at h
  contrapose! h
  obtain ⟨u, u_in, hu⟩ : ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ ∀ n m, m < n → u m ∉ ball (u n) V := by
    simp only [not_subset, mem_iUnion₂, not_exists, exists_prop] at h
    simpa only [forall_and, forall_mem_image, not_and] using seq_of_forall_finite_exists h
  refine ⟨u, u_in, fun x _ φ hφ huφ => ?_⟩
  obtain ⟨N, hN⟩ : ∃ N, ∀ p q, p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V :=
    huφ.cauchySeq.mem_entourage V_in
  exact hu (φ <| N + 1) (φ N) (hφ <| Nat.lt_add_one N) (hN (N + 1) N N.le_succ le_rfl)
Sequential Compactness Implies Total Boundedness in Uniform Spaces
Informal description
If a subset $s$ of a uniform space is sequentially compact, then it is totally bounded. That is, for every entourage $E$ in the uniformity, there exists a finite subset $F \subseteq s$ such that $s$ is covered by the union of $E$-balls centered at points of $F$.
IsSeqCompact.isComplete theorem
(hs : IsSeqCompact s) : IsComplete s
Full source 
/-- A sequentially compact set in a uniform set with countably generated uniformity filter
is complete. -/
protected theorem IsSeqCompact.isComplete (hs : IsSeqCompact s) : IsComplete s := fun l hl hls => by
  have := hl.1
  rcases exists_antitone_basis (𝓤 X) with ⟨V, hV⟩
  choose W hW hWV using fun n => comp_mem_uniformity_sets (hV.mem n)
  have hWV' : ∀ n, W n ⊆ V n := fun n ⟨x, y⟩ hx =>
    @hWV n (x, y) ⟨x, refl_mem_uniformity <| hW _, hx⟩
  obtain ⟨t, ht_anti, htl, htW, hts⟩ :
      ∃ t : ℕ → Set X, Antitone t ∧ (∀ n, t n ∈ l) ∧ (∀ n, t n ×ˢ t n ⊆ W n) ∧ ∀ n, t n ⊆ s := by
    have : ∀ n, ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s := by
      rw [le_principal_iff] at hls
      have : ∀ n, W n ∩ s ×ˢ sW n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)
      simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff,
        prod_self_subset_prod_self, and_assoc] using this
    choose t htl htW hts using this
    have : ∀ n : ℕ, ⋂ k ≤ n, t k⋂ k ≤ n, t k ⊆ t n := fun n => by apply iInter₂_subset; rfl
    exact ⟨fun n => ⋂ k ≤ n, t k, fun m n h =>
      biInter_subset_biInter_left fun k (hk : k ≤ m) => hk.trans h, fun n =>
      (biInter_mem (finite_le_nat n)).2 fun k _ => htl k, fun n =>
      (prod_mono (this n) (this n)).trans (htW n), fun n => (this n).trans (hts n)⟩
  choose u hu using fun n => Filter.nonempty_of_mem (htl n)
  have huc : CauchySeq u := hV.toHasBasis.cauchySeq_iff.2 fun N _ =>
      ⟨N, fun m hm n hn => hWV' _ <| @htW N (_, _) ⟨ht_anti hm (hu _), ht_anti hn (hu _)⟩⟩
  rcases hs.exists_tendsto (fun n => hts n (hu n)) huc with ⟨x, hxs, hx⟩
  refine ⟨x, hxs, (nhds_basis_uniformity' hV.toHasBasis).ge_iff.2 fun N _ => ?_⟩
  obtain ⟨n, hNn, hn⟩ : ∃ n, N ≤ n ∧ u n ∈ ball x (W N) :=
    ((eventually_ge_atTop N).and (hx <| ball_mem_nhds x (hW N))).exists
  refine mem_of_superset (htl n) fun y hy => hWV N ⟨u n, hn, htW N ?_⟩
  exact ⟨ht_anti hNn (hu n), ht_anti hNn hy⟩
Sequential Compactness Implies Completeness in Uniform Spaces
Informal description
Let $X$ be a uniform space with a countably generated uniformity filter, and let $s \subseteq X$ be a sequentially compact subset. Then $s$ is complete, meaning every Cauchy sequence in $s$ converges to a point in $s$.
IsSeqCompact.isCompact theorem
(hs : IsSeqCompact s) : IsCompact s
Full source 
/-- If `𝓤 β` is countably generated, then any sequentially compact set is compact. -/
protected theorem IsSeqCompact.isCompact (hs : IsSeqCompact s) : IsCompact s :=
  isCompact_iff_totallyBounded_isComplete.2 ⟨hs.totallyBounded, hs.isComplete⟩
Sequential Compactness Implies Compactness in Uniform Spaces with Countably Generated Uniformity
Informal description
Let $X$ be a uniform space with a countably generated uniformity filter, and let $s \subseteq X$ be a sequentially compact subset. Then $s$ is compact.
UniformSpace.isCompact_iff_isSeqCompact theorem
: IsCompact s ↔ IsSeqCompact s
Full source 
/-- A version of Bolzano-Weierstrass: in a uniform space with countably generated uniformity filter
(e.g., in a metric space), a set is compact if and only if it is sequentially compact. -/
protected theorem UniformSpace.isCompact_iff_isSeqCompact : IsCompactIsCompact s ↔ IsSeqCompact s :=
  ⟨fun H => H.isSeqCompact, fun H => H.isCompact⟩
Equivalence of Compactness and Sequential Compactness in Uniform Spaces with Countably Generated Uniformity
Informal description
Let $X$ be a uniform space with a countably generated uniformity filter, and let $s \subseteq X$ be a subset. Then $s$ is compact if and only if $s$ is sequentially compact.