lean_workbook_plus_47099

Proved

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

Let $x_1=\sqrt{2}$ and $x_{n+1}=\sqrt{2+x_n}$ . Show by induction that $x_n < x_{n+1}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_47099 (n : ℕ) (f : ℕ → ℝ) (hf: f 0 = Real.sqrt 2 ∧ ∀ n, f (n + 1) = Real.sqrt (2 + f n)) : f n < f (n + 1)   :=  by sorry

Source