two_mul_le_exp — Mathlib

English

For all real x, 2x ≤ exp x.

Русский

Для всех действительных x: 2x ≤ exp(x).

LaTeX

$$$2x \le \exp(x)$$$

Lean4

theorem two_mul_le_exp {x : ℝ} : 2 * x ≤ exp x :=
  by
  by_cases hx0 : x < 0
  · exact le_trans (mul_nonpos_of_nonneg_of_nonpos (by simp only [Nat.ofNat_nonneg]) hx0.le) (exp_nonneg x)
  · apply le_trans (mul_le_mul_of_nonneg_right _ (le_of_not_gt hx0)) exp_one_mul_le_exp
    have := Real.add_one_le_exp 1
    rwa [one_add_one_eq_two] at this

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