Prove2Me

Lean-Workbook Plus 34337: Logarithmic inequality

Proved
WorkbookRestored.plus_34337

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

lean-workbookrestored-importssource-checked

For real x≥1x\ge1, 1−1/x≤log⁡x<1+x1-1/x\le\log x<1+x.

Source: Lean-Workbook row lean_workbook_plus_34337 (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_34337 (x : ℝ) (hx : 1 ≤ x) : 1 - 1 / x ≤ Real.log x ∧ Real.log x < 1 + x   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_34337; immutable original Prove2Me node 5ab09bee-aa75-4193-aaa6-0a2f484fe9fe

View graph