rpow_ofNNReal

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#ENNReal.rpow_ofNNReal

English

For M ∈ NNReal and P ∈ ℝ with P ≥ 0, (M)^P = ↑(M^P).

Русский

Для M ∈ NNReal и P ∈ ℝ с P ≥ 0, (M)^P = ↑(M^P).

LaTeX

$$$(M: \\mathbb{R}_{\\ge 0})^{P} = ↑(M^{P}) \\quad (P \\ge 0)$$$

Lean4

theorem rpow_ofNNReal {M : ℝ≥0} {P : ℝ} (hP : 0 ≤ P) : (M : ℝ≥0∞) ^ P = ↑(M ^ P) := by
  rw [ENNReal.coe_rpow_of_nonneg _ hP, ← ENNReal.rpow_eq_pow]

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

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

Разделы

Аффилиация

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