lean_workbook_plus_4758

Open

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

We have $\forall x\ge 1, e^{-x}\le 1\implies 1+e^{-x}\le 2\implies \frac{2}{x(1+e^{-x})}\ge \frac{1}{x}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4758 : ∀ x : ℝ, 1 ≤ x → 2 / (x * (1 + exp (-x))) ≥ 1 / x   :=  by sorry

Source