English
From a subsequence frequently visiting a sequentially compact set, one can extract a convergent subsequence to a point in the set.
Русский
Из подпоследовательности, часто встречающейся в последовательнос-замкнутом множестве, можно извлечь сходящуюся подпоследовательность к точке множества.
LaTeX
$$$\text{IsSeqCompact}(s) \to (\exists^\text{freq} n \in \text{atTop}, x_n \in s) \to \exists a\in s, \exists \phi: \mathbb{N} \to \mathbb{N}, \text{StrictMono}(\phi) \land \text{Tendsto}(x \circ \phi) \text{ atTop } (\mathcal{N}(a))$$$
Lean4
theorem 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⟩
