Lean-Workbook Plus 80534: Exponential inequality

Proved

WorkbookRestored.plus_80534

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

lean-workbookrestored-importssource-checked

for all $0<x<1$ , the following inequality is valid: $e^{x} < \frac{1}{1-x}$ .

Source: Lean-Workbook row lean_workbook_plus_80534 (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_80534 (x : ℝ) (hx_pos : 0 < x) (hx_lt_one : x < 1) : exp x < 1 / (1 - x)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_80534; immutable original Prove2Me node d7b1ac09-cf62-44ba-859c-d61db227982d

View graph