lean_workbook_plus_26494

Proved

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

prove that: \n\n $\frac{2}{3}(x+y+z)\geq(y+x)(y+z)(z+x)$ \n\n $x,y,z \in (0,\frac{1}{2}]$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_26494 (x y z : ℝ) (hx : x ∈ Set.Icc 0 (1 / 2)) (hy : y ∈ Set.Icc 0 (1 / 2)) (hz : z ∈ Set.Icc 0 (1 / 2)) : (2 / 3) * (x + y + z) ≥ (y + x) * (y + z) * (z + x)   :=  by sorry

Source

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

View graph