English
Let X be a pseudo-metric space. If every Cauchy sequence in X converges (i.e., has a limit with respect to the topology of X), then X is a complete space.
Русский
Пусть X — псевдометрическое пространство. Если каждая последовательность Коши в X сходится (то есть имеет предел в топологии X), то X является полным пространством.
LaTeX
$$$\\displaystyle \\Bigl( \\forall u: \\mathbb{N} \\to X\\,,\\; \\text{CauchySeq}(u) \\Rightarrow \\exists a,\\; \\text{Tendsto}(u\\text{ atTop})(\\mathcal{N} a) \\Bigr) \\Rightarrow \\text{CompleteSpace}(X).$$$
Lean4
/-- A pseudo-metric space is complete iff every Cauchy sequence converges. -/
theorem complete_of_cauchySeq_tendsto : (∀ u : ℕ → α, CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)) → CompleteSpace α :=
EMetric.complete_of_cauchySeq_tendsto
