cauchySeq_iff — Mathlib

English

A sequence u is Cauchy if and only if for every ε > 0 there exists N such that for all m,n ≥ N we have ∥u_m / u_n∥ < ε.

Русский

Последовательность u есть таковой что ∥u_m / u_n∥<ε, когда m,n ≥ N.

LaTeX

$$CauchySeq u ↔ ∀ ε>0, ∃ N, ∀ m≥N, ∀ n≥N, ‖u_m / u_n‖ < ε$$

Lean4

@[to_additive]
theorem cauchySeq_iff [Nonempty α] [SemilatticeSup α] {u : α → E} :
    CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → ‖u m / u n‖ < ε := by
  simp [Metric.cauchySeq_iff, dist_eq_norm_div]

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