abs_rpow_le_abs_rpow — Mathlib

English

For all x,y, |x^y| ≤ |x|^y.

Русский

Для всех x,y выполняется |x^y| ≤ |x|^y.

LaTeX

$$$\\forall x,y \\in \\mathbb{R}, |x^y| \le |x|^y$$$

Lean4

@[bound]
theorem abs_rpow_le_abs_rpow (x y : ℝ) : |x ^ y| ≤ |x| ^ y :=
  by
  rcases le_or_gt 0 x with hx | hx
  · rw [abs_rpow_of_nonneg hx]
  · rw [abs_of_neg hx, rpow_def_of_neg hx, rpow_def_of_pos (neg_pos.2 hx), log_neg_eq_log, abs_mul,
      abs_of_pos (exp_pos _)]
    exact mul_le_of_le_one_right (exp_pos _).le (abs_cos_le_one _)

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