lean_workbook_plus_36307

Proved

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

$\dfrac{1}{\sqrt{n}}>2(\sqrt{n+1}-\sqrt{n})$ (directly or using the mean value theorem for $f(x)=\sqrt{x}$ and the interval $[n,n+1])$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source