lean_workbook_plus_40274

Proved

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

by AM-GM $ab\le \frac{a^{2}+b^{2}}{2}$ $ac\le \frac{a^{2}+c^{2}}{2}$ $bc\le \frac{b^{2}+c^{2}}{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40274 (a b c: ℝ) : a * b ≤ (a ^ 2 + b ^ 2) / 2 ∧ a * c ≤ (a ^ 2 + c ^ 2) / 2 ∧ b * c ≤ (b ^ 2 + c ^ 2) / 2   :=  by sorry

Source