le_inv_mul_exp

Mathlib.Analysis.Complex.Exponential

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

← MathLib Explorer

English

For x ∈ ℝ and c > 0, x ≤ c^{-1} exp(c x).

Русский

Для x ∈ ℝ и c > 0 выполнено x ≤ c^{-1} exp(c x).

LaTeX

$$$x \\leq c^{-1} \\exp(c x) \\quad (c > 0).$$$

Lean4

theorem le_inv_mul_exp (x : ℝ) {c : ℝ} (hc : 0 < c) : x ≤ c⁻¹ * exp (c * x) :=
  by
  rw [le_inv_mul_iff₀ hc]
  calc
    c * x
    _ ≤ c * x + 1 := (le_add_of_nonneg_right zero_le_one)
    _ ≤ _ := Real.add_one_le_exp (c * x)

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

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

Разделы

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

Аффилиация

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