The exponential lies strictly above its tangent

Proved

WorkbookRestored.plus_687

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

lean-workbookrestored-importssource-checked

For every real $x>0$ ,

e^x>x+1.

Formalization Note This restores source entry lean_workbook_plus_687 from the Apache-2.0 Lean-Workbook dataset. The mathematical proposition is unchanged; targeted imports and namespace openings supply the constants missing from the original Prove2Me node e88c1117-de7b-4024-aef3-39a3bb4379a2. This is a separate corrected node because formal statements and preambles are immutable.

Preamble

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

Formal statement

theorem WorkbookRestored.plus_687 (x : ℝ) (hx : x > 0) : Real.exp x > x + 1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_687; original Prove2Me theorem ID e88c1117-de7b-4024-aef3-39a3bb4379a2; Apache-2.0.

View graph