nnrpow_le_nnrpow

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

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

English

If a ≤ b and p ∈ [0,1], then a^p ≤ b^p for NNReal exponents in a C*-algebra.

Русский

Если a ≤ b и p ∈ [0,1], тогда a^p ≤ b^p для NNReal степеней в C*-алгебре.

LaTeX

$$$a \\le b \\Rightarrow a^{p} \\le b^{p}$, $p ∈ Icc(0,1)$$$

Lean4

@[gcongr]
theorem nnrpow_le_nnrpow {p : ℝ≥0} (hp : p ∈ Icc 0 1) {a b : A} (hab : a ≤ b) : a ^ p ≤ b ^ p :=
  monotone_nnrpow hp hab

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

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

Разделы

Аффилиация

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