exp_abs_le

Mathlib.Analysis.Complex.Exponential

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

English

For all real x, exp(|x|) ≤ exp(x) + exp(-x).

Русский

Для всех x из R верно: exp(|x|) ≤ exp(x) + exp(-x).

LaTeX

$$$\exp(|x|) \le \exp(x) + \exp(-x)$$$

Lean4

theorem exp_abs_le (x : ℝ) : exp |x| ≤ exp x + exp (-x) := by
  cases le_total x 0 <;> simp [abs_of_nonpos, abs_of_nonneg, exp_nonneg, *]

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

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

Разделы

Аффилиация

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