English
Let X be a topological space with the First Countable property. If s is a compact subset of X and a sequence x_n takes values in s infinitely often, then there exists a ∈ s and a strictly increasing function φ: N → N such that the subsequence x_{φ(n)} converges to a (i.e., x_{φ(n)} → a).
Русский
Пусть X — топологическое пространство с свойством последовательной считываемости (First Countable). Пусть s ⊆ X компактно и последовательность x_n принимает значения в s бесконечно часто. Тогда существует a ∈ s и строго возрастающая отображение φ: N → N such that последовательность x_{φ(n)} сходится к a (x_{φ(n)} → a).
LaTeX
$$$\forall X [TopologicalSpace X] [FirstCountableTopology X], \forall s \subseteq X, IsCompact s \to (\exists \text{ frequently } n \text{ in } atTop, x_n \in s) \to \exists a \in s, \exists φ : \mathbb{N} \to \mathbb{N}, \text{StrictMono } φ \land \text{Tendsto } (x \circ φ) \text{ atTop } (\mathcal{N} a).$$$
Lean4
theorem 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
