lean_workbook_plus_69452

Proved

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

If $a + b = c$ , then $a^2 + b^2 \geq \frac {c^2}{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_69452 (a b c : ℝ) (hab : a + b = c) : a^2 + b^2 ≥ c^2 / 2   :=  by sorry

Source