lean_workbook_plus_41996

Proved

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

Prove that $0 < \frac{a+d}{1+\frac{ad}{c^2}} < c$ given $c>0$ , $0<a<c$ , and $0<d<c$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_41996    (a d c : ℝ) (hc : 0 < c) (ha : 0 < a ∧ a < c) (hd : 0 < d ∧ d < c)
    (had : a * d < c^2) :
  0 < (a + d) / (1 + a * d / c^2) ∧ (a + d) / (1 + a * d / c^2) < c   :=  by sorry

Source

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

View graph