sqrt_le_sqrt

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

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

English

The square root function is operator monotone on the positive cone of a C*-algebra.

Русский

Квадратный корень является операторно-монтонной на положительном коне C*-алгебры.

LaTeX

$$$\\text{monotone}(\\sqrt)\\;\\text{on }\\{a\\ge 0\\}$$$

Lean4

@[gcongr]
theorem sqrt_le_sqrt (a b : A) (hab : a ≤ b) : sqrt a ≤ sqrt b :=
  monotone_sqrt hab

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

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

Разделы

Аффилиация

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