ofReal_rpow_of_pos — Mathlib

English

If x > 0 (real) and p ∈ ℝ, then (ENNReal.ofReal x)^p = ENNReal.ofReal(x^p).

Русский

Если x > 0 (как число) и p ∈ ℝ, тогда (ENNReal.ofReal x)^p = ENNReal.ofReal(x^p).

LaTeX

$$$ (ENNReal.ofReal x)^p = ENNReal.ofReal (x^p) $$$

Lean4

theorem ofReal_rpow_of_pos {x p : ℝ} (hx_pos : 0 < x) : ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p) :=
  by
  simp_rw [ENNReal.ofReal]
  rw [← coe_rpow_of_ne_zero, coe_inj, Real.toNNReal_rpow_of_nonneg hx_pos.le]
  simp [hx_pos]

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