lean_workbook_plus_21743

Proved

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

Find the maximum or minimum value of the expression $\frac{x}{1+yz}+\frac{y}{1+xz}+\frac{z}{1+xy}$ given that $x, y, z > 0$ and $x^2+y^2+z^2=1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_21743 (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (hx2 : x ^ 2 + y ^ 2 + z ^ 2 = 1) : (x / (1 + y * z) + y / (1 + x * z) + z / (1 + x * y) ≤ 1 ∨ x / (1 + y * z) + y / (1 + x * z) + z / (1 + x * y) ≥ 1)   :=  by sorry

Source

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

View graph