nnrpow

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

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

← MathLib Explorer

English

For a, x with x ∈ ℝ≥0, a^x is nonnegative: 0 ≤ a^x.

Русский

Для любого a и x ∈ ℝ≥0 выполняется ≥ 0: a^x ≥ 0.

LaTeX

$$0 ≤ a ^ x$$

Lean4

/-- Real powers of operators, based on the non-unital continuous functional calculus. -/
noncomputable def nnrpow (a : A) (y : ℝ≥0) : A :=
  cfcₙ (NNReal.nnrpow · y) a

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

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

Разделы

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

Аффилиация

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