lean_workbook_plus_23528

Open

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

Use the inequality $\ln{x}<x-1<\dfrac{x-1}{2-x}$ when $x\in(0,1)$ and we're done.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23528 (x : ℝ) (hx : 0 < x ∧ x < 1) :
  Real.log x < x - 1 ∧ x - 1 < (x - 1) / (2 - x)   :=  by sorry

Source