rpow_max — Mathlib

English

For nonnegative x, y and p, (max{x,y})^p = max{x^p, y^p}.

Русский

Для неотрицательных x, y и p выполняется (макс{x,y})^p = max{x^p, y^p}.

LaTeX

$$$(0 \le x) \land (0 \le y) \land (0 \le p) \Rightarrow (\max\{x,y\})^{p} = \max\{x^{p}, y^{p}\}$$$

Lean4

theorem rpow_max {x y p : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hp : 0 ≤ p) : (max x y) ^ p = max (x ^ p) (y ^ p) :=
  by
  rcases le_total x y with hxy | hxy
  · rw [max_eq_right hxy, max_eq_right (rpow_le_rpow hx hxy hp)]
  · rw [max_eq_left hxy, max_eq_left (rpow_le_rpow hy hxy hp)]

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