ofReal_pow — Mathlib

English

For p ≥ 0 and n ∈ ℕ, ENNReal.ofReal(p^n) = ENNReal.ofReal(p)^n.

Русский

Для p ≥ 0 и натурального n: ENNReal.ofReal(p^n) = ENNReal.ofReal(p)^n.

LaTeX

$$$p \ge 0 \Rightarrow \operatorname{ofReal}(p^n) = \operatorname{ofReal}(p)^n$$$

Lean4

@[simp]
theorem ofReal_pow {p : ℝ} (hp : 0 ≤ p) (n : ℕ) : ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n := by
  rw [ofReal_eq_coe_nnreal hp, ← coe_pow, ← ofReal_coe_nnreal, NNReal.coe_pow, NNReal.coe_mk]

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