cfcHom_mono

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

URI: https://scilib.ai/kg/mathlib#cfcHom_mono

English

If f ≤ g as functions on the spectrum, then cfcHom ha f ≤ cfcHom ha g for fixed a with ha.

Русский

Если f ≤ g на спектре, то cfcHom ha f ≤ cfcHom ha g для фиксированного a.

LaTeX

$$cfcHom ha f ≤ cfcHom ha g$$

Lean4

theorem cfcHom_mono {a : A} (ha : p a) {f g : C(spectrum R a, R)} (hfg : f ≤ g) : cfcHom ha f ≤ cfcHom ha g :=
  OrderHomClass.mono (cfcHom ha) hfg

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

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

Разделы

Аффилиация

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