cauchySeq_of_le_geometric_two — Mathlib

English

If dist(f n, f(n+1)) ≤ C/2^{n} then Cauchy.

Русский

Если dist(f_n, f_{n+1}) ≤ C/2^{n}, то последовательность является Cauchy.

LaTeX

$$$$\text{Cauchy}(f)\;\text{when} \;dist(f_n,f_{n+1}) \le C/2^n.$$$$

Lean4

/-- If `dist (f n) (f (n+1))` is bounded by `(C / 2) / 2^n`, then `f` is a Cauchy sequence. -/
theorem cauchySeq_of_le_geometric_two : CauchySeq f :=
  cauchySeq_of_dist_le_of_summable _ hu₂ <| ⟨_, hasSum_geometric_two' C⟩

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