toNNReal_zpow — Mathlib

English

If x ≥ 0, then (x^n).toNNReal = x.toNNReal^n for all integers n.

Русский

Если x ≥ 0, то (x^n).toNNReal = (x.toNNReal)^n для всех целых n.

LaTeX

$$$$ x \ge 0 \implies (x^n)^{\mathrm{toNNReal}} = (x^{\mathrm{toNNReal}})^n, \quad n \in \mathbb{Z}. $$$$

Lean4

theorem toNNReal_zpow {x : ℝ} (hx : 0 ≤ x) (n : ℤ) : (x ^ n).toNNReal = x.toNNReal ^ n := by
  rw [← coe_inj, NNReal.coe_zpow, Real.coe_toNNReal _ (zpow_nonneg hx _), Real.coe_toNNReal x hx]

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