lean_workbook_plus_37200

Proved

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

prove that:\n $\frac {4x}{y + z}\leq x(\frac {1}{y} + \frac {1}{z})$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_37200 {x y z : ℝ} (hx : x > 0) (hy : y > 0) (hz : z > 0) : 4 * x / (y + z) ≤ x * (1 / y + 1 / z)   :=  by sorry

Source