nnrpow_eq_rpow

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

URI: https://scilib.ai/kg/mathlib#CFC.nnrpow_eq_rpow

English

If x > 0 in NNReal, then a^x = a^{x.toReal}.

Русский

Если x > 0 в NNReal, то a^x = a^{x.toReal}.

LaTeX

$$Eq (a ^ x) (a ^ x.toReal)$$

Lean4

theorem nnrpow_eq_rpow {a : A} {x : ℝ≥0} (hx : 0 < x) : a ^ x = a ^ (x : ℝ) := by
  rw [nnrpow_def (A := A), rpow_def, cfcₙ_eq_cfc]

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

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

Разделы

Аффилиация

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