toNNReal_rpow_of_nonneg

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

← MathLib Explorer

English

For nonnegative x, Real.toNNReal(x^y) = Real.toNNReal(x)^y.

Русский

Пусть x ≥ 0. Тогда Real.toNNReal(x^y) = Real.toNNReal(x)^y.

LaTeX

$$$x \\ge 0 \\Rightarrow \\operatorname{toNNReal}(x^y) = \\operatorname{toNNReal}(x)^y$$$

Lean4

theorem _root_.Real.toNNReal_rpow_of_nonneg {x y : ℝ} (hx : 0 ≤ x) : Real.toNNReal (x ^ y) = Real.toNNReal x ^ y :=
  by
  nth_rw 1 [← Real.coe_toNNReal x hx]
  rw [← NNReal.coe_rpow, Real.toNNReal_coe]

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

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

Разделы

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

Аффилиация

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