Lean-Workbook Plus 5840: Logarithmic inequality

Proved

WorkbookRestored.plus_5840

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For every real $x<1$ , $x+\log(1-x)\le0$ . This statement formalizes the inequality component of the source; the source also asks to characterize equality.

Source: Lean-Workbook row lean_workbook_plus_5840 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Real

Formal statement

theorem WorkbookRestored.plus_5840 (x : ℝ) (hx : x < 1) : x + Real.log (1 - x) ≤ 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_5840; immutable original Prove2Me node e7354be3-3d9f-42e3-a521-3746aad45f60

View graph