lean_workbook_plus_80534

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

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

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_80534 (x : ℝ) (hx_pos : 0 < x) (hx_lt_one : x < 1) : exp x < 1 / (1 - x)   :=  by sorry

Source