nnrpow_def

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

URI: https://scilib.ai/kg/mathlib#NNReal.nnrpow_def

English

For fixed y in NNReal, the map x ↦ nnrpow x y is continuous: Continuous (nnrpow · y).

Русский

Для фиксированного y в NNReal отображение x ↦ nnrpow x y непрерывно.

LaTeX

$$Continuous (nnrpow · y)$$

Lean4

@[simp]
theorem nnrpow_def (a b : ℝ≥0) : nnrpow a b = a ^ (b : ℝ) :=
  rfl

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

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

Разделы

Аффилиация

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