toNNReal_rpow — Mathlib

English

For ENNReal x and real z, (toReal (x^z)) equals (toReal x)^z.

Русский

Для ENNReal x и вещественного z, toReal(x^z) равно (toReal x)^z.

LaTeX

$$$ (x^z).toReal = x^{z}.toReal $$$

Lean4

@[simp]
theorem toNNReal_rpow (x : ℝ≥0∞) (z : ℝ) : (x ^ z).toNNReal = x.toNNReal ^ z :=
  by
  rcases lt_trichotomy z 0 with (H | H | H)
  ·
    cases x with
    | top => simp [H, ne_of_lt]
    | coe x =>
      by_cases hx : x = 0
      · simp [hx, H, ne_of_lt]
      · simp [← coe_rpow_of_ne_zero hx]
  · simp [H]
  · cases x
    · simp [H, ne_of_gt]
    simp [← coe_rpow_of_nonneg _ (le_of_lt H)]

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