coe_rpow_of_nonneg — Mathlib

English

If x ≥ 0 and y ≥ 0, then ↑(x^y) = (↑x)^y in ENNReal.

Русский

Если x ≥ 0 и y ≥ 0, то ↑(x^y) = (↑x)^y в ENNReal.

LaTeX

$$$(\\uparrow x^y) = (\\uparrow x)^y , \\quad x \\ge 0,\\ y \\ge 0$$$

Lean4

@[norm_cast]
theorem coe_rpow_of_nonneg (x : ℝ≥0) {y : ℝ} (h : 0 ≤ y) : ↑(x ^ y) = (x : ℝ≥0∞) ^ y :=
  by
  by_cases hx : x = 0
  · rcases le_iff_eq_or_lt.1 h with (H | H)
    · simp [hx, H.symm]
    · simp [hx, zero_rpow_of_pos H, NNReal.zero_rpow (ne_of_gt H)]
  · exact coe_rpow_of_ne_zero hx _

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