lean_workbook_plus_71452

Proved

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

so $x+3 \leq \sqrt{2(x^2+10)}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71452 (x : ℝ) : x + 3 ≤ Real.sqrt (2 * (x ^ 2 + 10))   :=  by sorry

Source