lean_workbook_plus_55695

Proved

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

Prove that $\sqrt{a}+\sqrt{b} \le \sqrt{2(a+b)}$ using AM-GM inequality.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55695 (a b : ℝ) (hab : 0 ≤ a ∧ 0 ≤ b) : Real.sqrt a + Real.sqrt b ≤ Real.sqrt (2 * (a + b))   :=  by sorry

Source