lean_workbook_plus_20955

Open

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

For $0<u<1,$ prove that $\ln(1-u)<-u$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20955 (u : ℝ) (h : 0 < u) (h' : u < 1) : Real.log (1 - u) < -u   :=  by sorry

Source