English
In a pseudo-emetric space, a Cauchy sequence u is characterized by: for every ε ∈ ℝ≥0 with 0 < ε, there exists N such that ∀ n ≥ N, edist(u n, u N) < ε.
Русский
В псевдоэметрическом пространстве последовательность Коши определяется так: для каждого ε ∈ ℝ≥0 с ε > 0 существует N, такое что для всех n ≥ N выполняется edist(u n, u N) < ε.
LaTeX
$$CauchySeq u \iff ∀ ε : ℝ≥0, 0 < ε → ∃ N, ∀ n, N ≤ n → edist (u n) (u N) < ε$$
Lean4
/-- A variation of the emetric characterization of Cauchy sequences that deals with
`ℝ≥0` upper bounds. -/
theorem cauchySeq_iff_NNReal [Nonempty β] [SemilatticeSup β] {u : β → α} :
CauchySeq u ↔ ∀ ε : ℝ≥0, 0 < ε → ∃ N, ∀ n, N ≤ n → edist (u n) (u N) < ε :=
uniformity_basis_edist_nnreal.cauchySeq_iff'
