add_one_lt_exp — Mathlib

English

If 0 < x < 1, then exp x < 1/(1 − x).

Русский

Если 0 < x < 1, то exp x < 1/(1 − x).

LaTeX

$$$\\text{Real.exp bound under strict interval: } 0 < x < 1 \\Rightarrow e^{x} < \\frac{1}{1 - x}.$$$

Lean4

theorem add_one_lt_exp {x : ℝ} (hx : x ≠ 0) : x + 1 < Real.exp x :=
  by
  obtain hx | hx := hx.symm.lt_or_gt
  · exact add_one_lt_exp_of_pos hx
  obtain h' | h' := le_or_gt 1 (-x)
  · linarith [x.exp_pos]
  have hx' : 0 < x + 1 := by linarith
  simpa [add_comm, exp_neg, inv_lt_inv₀ (exp_pos _) hx'] using exp_bound_div_one_sub_of_interval' (neg_pos.2 hx) h'

Похожие утверждения