seq_compact_of_compact — Mathlib

English

If X is a compact space, then every sequence x: N → X has a convergent subsequence; i.e., there exists a ∈ X and a strictly increasing φ: N → N such that x ∘ φ → a in the neighborhood sense.

Русский

Если X компактно, то любая последовательность x_n: N → X имеет сходящуюся подпоследовательность; т.е. существует a ∈ X и строго возрастающая φ: N → N такая, что x_{φ(n)} → a.

LaTeX

$$$[CompactSpace X] \to \Exists a \in X, \Exists φ: \mathbb{N} \to \mathbb{N}, \text{StrictMono } φ \land \text{Tendsto } (x \circ φ) atTop (\mathcal{N} a).$$$

Lean4

instance (priority := 100) seq_compact_of_compact [CompactSpace X] : SeqCompactSpace X :=
  ⟨isCompact_univ.isSeqCompact⟩

Похожие утверждения