lean_workbook_plus_43677

Proved

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

Prove that $(x+y+z)+3xyz\geq 2(xy+yz+zx)$ given $0\leq x,y,z\leq 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

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

View graph