lean_workbook_plus_18564

Proved

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

For $x,y,z\in\mathbb{R} ,x+y+z=4,$ show: $|x-1|+\frac{|y|+|y-2|}{2}\ge 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18564 (x y z : ℝ) (h : x + y + z = 4) : 1 ≤ |x - 1| + (|y| + |y - 2|) / 2   :=  by sorry

Source