lean_workbook_plus_23509

Proved

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

Determine the general term of the sequence ( $a_n$ ) given by $a_0 =\alpha > 0$ and $a_{n+1} =\frac{a_n}{1+a_n}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23509 (α : ℝ) (α_pos : 0 < α) : ∃ a : ℕ → ℝ, a 0 = α ∧ ∀ n, a (n + 1) = a n / (1 + a n)   :=  by sorry

Source