lean_workbook_plus_1369

Proved

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

$\frac{mz+nx}{m+n}\geq \frac{m+n}{\frac{m}{z}+\frac{n}{x}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1369 {m n z x : ℝ}
 (hm : 0 < m)
 (hn : 0 < n)
 (hz : 0 < z)
 (hx : 0 < x) :
 (m * z + n * x) / (m + n) ≥ (m + n) / (m / z + n / x)   :=  by sorry

Source

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

View graph