exp_bound_div_one_sub_of_interval

Mathlib.Analysis.Complex.Exponential

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

← MathLib Explorer

English

If 0 ≤ x < 1, then e^x ≤ 1/(1 − x).

Русский

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

LaTeX

$$$\\text{Real.exp bound under interval: } x \\in [0,1) \\,\\Rightarrow\\, e^{x} \\leq \\frac{1}{1 - x}.$$$

Lean4

theorem exp_bound_div_one_sub_of_interval {x : ℝ} (h1 : 0 ≤ x) (h2 : x < 1) : Real.exp x ≤ 1 / (1 - x) :=
  by
  rcases eq_or_lt_of_le h1 with (rfl | h1)
  · simp
  · exact (exp_bound_div_one_sub_of_interval' h1 h2).le

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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