lean_workbook_plus_37353

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that if $\sum_{i=0}^\infty a_i$ converges, then $\sum_{i=0}^\infty\frac{a_i}{a_i+1}$ converges, assuming $a_i > 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_37353 (a : ℕ → ℝ) (ha : ∀ i, a i > 0) (h : Summable a) : Summable (λ i => a i / (a i + 1))   :=  by sorry

Source