lean_workbook_plus_62898
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_62898 (x y z : ℝ) (h : 0 < x ∧ 0 < y ∧ 0 < z) : x * (1/y + 1/z) ≥ 4*x/(y+z) := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_62898 (x y z : ℝ) (h : 0 < x ∧ 0 < y ∧ 0 < z) : x * (1/y + 1/z) ≥ 4*x/(y+z) := by sorry