cauchySeq_of_le_geometric — Mathlib

English

In a seminormed additive group, if ∥u_n − u_{n+1}∥ ≤ C r^n with r < 1, then the sequence (u_n) is Cauchy.

Русский

В семинормированной аддитивной группе, если ∥u_n − u_{n+1}∥ ≤ C r^n с r < 1, то последовательность (u_n) является фундаментальной (численно сходится).

LaTeX

$$∀ C r, r < 1, ∀ u, ∀ n, ∥u(n) - u(n+1)∥ ≤ C r^n ⇒ CauchySeq u$$

Lean4

nonrec theorem cauchySeq_of_le_geometric {C : ℝ} {r : ℝ} (hr : r < 1) {u : ℕ → α}
    (h : ∀ n, ‖u n - u (n + 1)‖ ≤ C * r ^ n) : CauchySeq u :=
  cauchySeq_of_le_geometric r C hr (by simpa [dist_eq_norm] using h)

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