lean_workbook_plus_14464

Proved

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

Prove that, if $u_{n+1} = u_{n} +2$ for $n \in \mathbb{N}$ and $u_{1}=3$ , then $u_{n}= 2n+1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14464 (n : ℕ) (u : ℕ → ℕ) (h₁ : u 1 = 3) (h₂ : ∀ n, u (n+1) = u n + 2) : u n = 2 * n + 1   :=  by sorry

Source