lean_workbook_plus_82183

Proved

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

proofwiki

Prove that if $x,y,z$ are real numbers and $x+y+z=2$ and $xy+yz+zx=1$ then $x,y,z \in [0,\frac{4}{3}]$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82183 (x y z : ℝ) (h₁ : x + y + z = 2) (h₂ : x * y + y * z + z * x = 1) : x ∈ Set.Icc 0 (4/3) ∧ y ∈ Set.Icc 0 (4/3) ∧ z ∈ Set.Icc 0 (4/3)   :=  by sorry

Source

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

View graph