lean_workbook_plus_24072

Proved

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

Prove that $\max(\min(a,b),\min(a,c))+\max(a,\min(b,c)) \leq a+\max(b,c)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24072 (a b c : ℝ) : (max (min a b) (min a c)) + max a (min b c) ≤ a + max b c   :=  by sorry

Source