one_sub_lt_exp_neg

Mathlib.Analysis.Complex.Exponential

URI: https://scilib.ai/kg/mathlib#Real.one_sub_lt_exp_neg

English

For x ≠ 0, 1 − x < exp(−x).

Русский

Для x ≠ 0, 1 − x < exp(−x).

LaTeX

$$$1 - x < \\exp(-x) \\quad (x \\neq 0).$$$

Lean4

theorem one_sub_lt_exp_neg {x : ℝ} (hx : x ≠ 0) : 1 - x < exp (-x) :=
  (sub_eq_neg_add _ _).trans_lt <| add_one_lt_exp <| neg_ne_zero.2 hx

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru