lean_workbook_plus_7110

Proved

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

$\frac{mx+ny}{m+n}\geq \frac{m+n}{\frac{m}{x}+\frac{n}{y}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7110 {m n x y : ℝ} (hm : 0 < m) (hn : 0 < n) (hx : 0 < x) (hy : 0 < y) :
  (m * x + n * y) / (m + n) ≥ (m + n) / (m / x + n / y)   :=  by sorry

Source

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

View graph