English
For a sequentially compact set s in a uniform space, if a sequence u has all its terms in s and is Cauchy, then there exists x ∈ s such that u → x.
Русский
Для последовательнос-но компактного множества s в равномерном пространстве, если последовательность u имеет все члены в s и является Cauchy, то существует x ∈ s, такой что u → x.
LaTeX
$$$\forall {X} [UniformSpace X] {s:Set X}, IsSeqCompact s → \forall {u: \mathbb{N} \to X}, (∀ n, u(n) ∈ s) → CauchySeq u → \Exists x \in s, Tendsto u atTop (nhds x).$$$
Lean4
theorem 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
