lean_workbook_plus_73693

Proved

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

Let $a,b,c$ be any real numbers. Prove that $(a+b+c)^2\ge3\bigl(\min(a,b)\max(b,c)+\min(b,c)\max(c,a)+\min(c,a)\max(a,b)\bigr).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_73693 (a b c : ℝ) :
  (a + b + c) ^ 2 ≥ 3 * (min a b * max b c + min b c * max c a + min c a * max a b)   :=  by sorry

Source