cfcₙHom_id

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

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

English

Alternative expression of the same identity: cfcₙHom ha (.id (σₙ R a)) equals a in A.

Русский

Альтернативное выражение идентичности: cfcₙHom ha (.id (σₙ R a)) равно a в A.

LaTeX

$$cfcₙHom ha (.id (σₙ R a)) = a$$

Lean4

theorem cfcₙHom_id : cfcₙHom ha (.id (σₙ R a)) = a :=
  (NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose_spec.2.1

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

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

Разделы

Аффилиация

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