lean_workbook_plus_47216

Proved

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

Consider the following expansion\n\n $(x-a)(y-b)(z-b) \ge 0$ \n\n $\Leftrightarrow xyz +xb^2+ab(y+z) \ge ab^2+ ayz + b(xy+xz)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_47216 (x y z a b : ℝ) : (x - a) * (y - b) * (z - b) ≥ 0 ↔ x * y * z + x * b ^ 2 + a * b * (y + z) ≥ a * b ^ 2 + a * y * z + b * (x * y + x * z)   :=  by sorry

Source

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

View graph