lean_workbook_plus_26590

Proved

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

For positive fractions $\dfrac {a} {b} < \dfrac {c} {d}$ that is called the mediant (the name comes from the Farey sequence(s)), and we have $\dfrac {a} {b} < \dfrac {a+c} {b+d} < \dfrac {c} {d}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_26590 (a b c d : ℕ) (h₁ : 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d) (h₂ : a * d < b * c) : (a * d < b * c ∧ b * c < (a + c) * (b + d))   :=  by sorry

Source

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

View graph