English
Let X be a topological space with FirstCountable topology. If s ⊆ X is compact and every x_n lies in s (i.e., ∀n, x_n ∈ s), then there exists a ∈ s and a subsequence x_{φ(n)} that converges to a along atTop.
Русский
Пусть X — топологическое пространство с первой счетностью. Пусть s ⊆ X компактно и для последовательности x_n выполняется x_n ∈ s для всех n. Тогда существует a ∈ s и подпоследовательность x_{φ(n)}, строго возрастающая φ, такая, что x_{φ(n)} сходится к a.
LaTeX
$$$\forall X [TopologicalSpace X] [FirstCountableTopology X], \forall s \subseteq X, IsCompact s \to (∀ n, x_n ∈ s) \to \exists a \in s, \exists φ : \mathbb{N} \to \mathbb{N}, \text{StrictMono } φ \land \text{Tendsto } (x \circ φ) atTop (\mathcal{N} a).$$$
Lean4
theorem 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
