lean_workbook_plus_18746

Open

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

Prove that $\frac{u}{1+e^{-u}}<u$ for all $u>0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18746 (u : ℝ) (hu : 0 < u) : u / (1 + exp (-u)) < u   :=  by sorry

Source