lean_workbook_plus_81106

Proved

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

Let $x,y,z\geq 0,$ prove that $|x-y|+|y-z|+|z-x|\geq \frac{1}{2}( |x+y-2z|+|y+z-2x|+|z+x-2y|).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81106 (x y z : ℝ) : |x - y| + |y - z| + |z - x| ≥ 1 / 2 * (|x + y - 2 * z| + |y + z - 2 * x| + |z + x - 2 * y|)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph