toNNReal_pow

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#Real.toNNReal_pow

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$$ x \ge 0 \implies (x^n)^{\mathrm{toNNReal}} = (x^{\mathrm{toNNReal}})^n. $$$$

Lean4

theorem toNNReal_pow {x : ℝ} (hx : 0 ≤ x) (n : ℕ) : (x ^ n).toNNReal = x.toNNReal ^ n := by
  rw [← coe_inj, NNReal.coe_pow, Real.coe_toNNReal _ (pow_nonneg hx _), Real.coe_toNNReal x hx]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru