lean_workbook_plus_75669

Proved

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

Let $n$ be a positive integer, prove that\n $\sqrt{n+1} - \sqrt{n} < \frac{1}{2 \sqrt n}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75669 (n : ℕ) (hn : 0 < n) : (Real.sqrt (n + 1) - Real.sqrt n) < 1 / (2 * Real.sqrt n)   :=  by sorry

Source