lean_workbook_plus_19068

Proved

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

$\frac{my+nz}{m+n}\geq \frac{m+n}{\frac{m}{y}+\frac{n}{z}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19068 {m n y z : ℝ} (hm : 0 < m) (hn : 0 < n) (hy : 0 < y) (hz : 0 < z) :
  (m * y + n * z) / (m + n) ≥ (m + n) / (m / y + n / z)   :=  by sorry

Source

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

View graph