cfcₙAux_id

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

URI: https://scilib.ai/kg/mathlib#cfcₙAux_id

English

For any p and a with pa, the auxiliary map sends the unit of the spectrum to a: cfcₙAux hp₁ a ha (.id _) = a.

Русский

Для любых p и a с pa выполняется: cfcₙAux hp₁ a ha (id) = a.

LaTeX

$$$$ cfc\\_nAux hp\\_1 a ha (.id _) = a $$$$

Lean4

theorem cfcₙAux_id : cfcₙAux hp₁ a ha (.id _) = a :=
  cfcHom_id (hp₁.mpr ha)

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

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

Разделы

Аффилиация

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