rpow_nonneg

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

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

English

For any a and y ∈ ℝ, a^y is nonnegative whenever a is nonnegative in the operator sense.

Русский

Для любого a и y ∈ ℝ, a^y неотрицательно тогда и только тогда, когда a неотрицательно в спектре.

LaTeX

$$$0 \\le a^{y}$$$

Lean4

@[simp, grind]
theorem rpow_nonneg {a : A} {y : ℝ} : 0 ≤ a ^ y :=
  cfc_predicate _ a

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

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

Разделы

Аффилиация

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