English
A variation: Cauchy sequences can be characterized by eventual closeness to a fixed term, i.e., for every ε > 0 there exists N such that for all n ≥ N, edist(u n, u N) < ε.
Русский
Вариант: последовательности Коши характеризуются тем, что после некоторого индекса все элементы близки к фиксированному члену, т.е. для каждого ε > 0 существует N такое, что для всех n ≥ N выполняется edist(u n, u N) < ε.
LaTeX
$$CauchySeq u \iff ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) (u N) < ε$$
Lean4
/-- A variation around the emetric characterization of Cauchy sequences -/
theorem cauchySeq_iff' [Nonempty β] [SemilatticeSup β] {u : β → α} :
CauchySeq u ↔ ∀ ε > (0 : ℝ≥0∞), ∃ N, ∀ n ≥ N, edist (u n) (u N) < ε :=
uniformity_basis_edist.cauchySeq_iff'
