English
There is a variant characterization: a sequence is Cauchy iff for all ε>0 there exists N such that for all n≥N, dist(u_n, u_N) < ε.
Русский
Существует вариант характеристики: последовательность Коши тогда и только тогда, когда для каждого ε>0 существует N, такой что для всех n≥N выполняется dist(u_n, u_N) < ε.
LaTeX
$$$\\displaystyle \\text{CauchySeq}(u) \\iff \\forall \\varepsilon>0, \\exists N, \\forall n\\ge N,\\; \\operatorname{dist}(u_n, u_N) < \\varepsilon.$$$
Lean4
/-- A variation around the pseudometric characterization of Cauchy sequences -/
theorem cauchySeq_iff' {u : β → α} : CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε :=
uniformity_basis_dist.cauchySeq_iff'
