cauchySeq_iff — Mathlib

English

Let u: β → α with a pseudo-EMetric space structure on α. Then u is a Cauchy sequence iff for every ε > 0 there exists N such that for all m ≥ N and n ≥ N, edist(u m, u n) < ε.

Русский

Пусть u: β → α в псевдо-эметрическом пространстве. Тогда последовательность u является последовательностью Коши тогда и только тогда, когда для каждого ε > 0 существует N, такое что для всех m ≥ N и n ≥ N выполняется edist(u m, u n) < ε.

LaTeX

$$CauchySeq u \iff ∀ ε > 0, ∃ N, ∀ m \ge N, ∀ n \ge N, edist (u m) (u n) < ε$$

Lean4

/-- In a pseudoemetric space, Cauchy sequences are characterized by the fact that, eventually,
the pseudoedistance between its elements is arbitrarily small -/
theorem cauchySeq_iff [Nonempty β] [SemilatticeSup β] {u : β → α} :
    CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → edist (u m) (u n) < ε :=
  uniformity_basis_edist.cauchySeq_iff

Похожие утверждения