exp_one_mul_le_exp — Mathlib

English

For all x, e·x ≤ e^x, where e = exp(1).

Русский

Для всех x выполняется e·x ≤ e^x, где e = exp(1).

LaTeX

$$$e\,x \le \exp(x)\quad\text{where } e = \exp(1)$$$

Lean4

theorem exp_one_mul_le_exp {x : ℝ} : exp 1 * x ≤ exp x :=
  by
  by_cases hx0 : x ≤ 0
  · apply le_trans (mul_nonpos_of_nonneg_of_nonpos (exp_pos 1).le hx0) (exp_nonneg x)
  · have h := add_one_le_exp (log x)
    rwa [← exp_le_exp, exp_add, exp_log (lt_of_not_ge hx0), mul_comm] at h

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