English
In a proper metric space, every bounded sequence has a convergent subsequence; more precisely, if s is bounded and x is a sequence frequently in s, then there exists a ∈ closure(s) and a subsequence x ∘ φ converging to a for some strictly increasing φ.
Русский
В корректном метрическом пространстве каждая ограниченная последовательность имеет сходящуюся подпоследовательность; если последовательность часто попадает в ограниченное множество s, существует предельная точка a ∈ closure(s) и подпоследовательность, сходящаяся к a.
LaTeX
$$$\\text{IsBounded}(s) \\Rightarrow \\forall x: \\mathbb{N} \\to X, \\ (\\exists \\text{ frequently in } s\, x) \\Rightarrow \\exists a \\in \\overline{s}, \\exists \\phi: \\mathbb{N} \\to \\mathbb{N}, \\text{StrictMono}(\\phi) \\land \\operatorname{Tendsto}(x \\circ \\phi) atTop (\\mathcal{N}(a)).$$$
Lean4
/-- A version of **Bolzano-Weierstrass**: in a proper metric space (e.g. $ℝ^n$),
every bounded sequence has a converging subsequence. -/
theorem tendsto_subseq_of_bounded (hs : IsBounded s) {x : ℕ → X} (hx : ∀ n, x n ∈ s) :
∃ a ∈ closure s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) :=
tendsto_subseq_of_frequently_bounded hs <| Frequently.of_forall hx
