lean_workbook_plus_38180

Proved

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

Now lets say $0<b_i<x$ so it can be said that $\frac{b_i}{b_i+2} \le \frac{x}{x+2} < 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_38180 (x : ℝ) (b_i : ℝ) (h₁ : 0 < b_i) (h₂ : b_i < x) : (b_i / (b_i + 2)) ≤ (x / (x + 2)) ∧ (x / (x + 2)) < 1   :=  by sorry

Source

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

View graph