summable_geometric_of_lt_one — Mathlib

English

If r ≥ 0 and r < 1, then the geometric sequence r^n is summable.

Русский

Если r ≥ 0 и r < 1, то геометрическая последовательность r^n суммируема.

LaTeX

$$$\\\\forall r \\\\in \\\\mathbb{R}, \\\\ 0 \\\\le r \\\\wedge r < 1 \\\\Rightarrow Summable (n \\\\mapsto r^n).$$$

Lean4

theorem summable_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : Summable fun n : ℕ ↦ r ^ n :=
  ⟨_, hasSum_geometric_of_lt_one h₁ h₂⟩

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