Lean-Workbook Plus 14760: Logarithmic inequality

Proved

WorkbookRestored.plus_14760

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

lean-workbookrestored-importssource-checked

If $u>0$ and $u\ne1$ , then $u-1-\log u>0$ .

Source: Lean-Workbook row lean_workbook_plus_14760 (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_14760 (u : ℝ) (h : 0 < u) (h' : u ≠ 1) : u - 1 - Real.log u > 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_14760; immutable original Prove2Me node 8cf63902-792e-4156-b0ee-c7719cb8a551

View graph