coe_ennreal_pow — Mathlib

English

Powers commute with the EReal embedding for ENNReal numbers: for x ∈ ENNReal and n ∈ ℕ, ↑(x^n) = (↑x)^n in EReal.

Русский

Степени для ENNReal совместимы с встраиванием в EReal: ↑(x^n) = (↑x)^n в EReal.

LaTeX

$$$ (\uparrow (x^n) : \mathrm{EReal}) = (\uparrow x : \mathrm{EReal})^n \quad (x \in \mathbb{R}_{≥0}^{\infty}, \ n \in \mathbb{N}) $$$

Lean4

@[simp, norm_cast]
theorem coe_ennreal_pow (x : ℝ≥0∞) (n : ℕ) : (↑(x ^ n) : EReal) = (x : EReal) ^ n :=
  map_pow (⟨⟨(↑), coe_ennreal_one⟩, coe_ennreal_mul⟩ : ℝ≥0∞ →* EReal) _ _

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