cfcHom_eq_of_isStarNormal — Mathlib

English

The map sending the identity function to a under continuous functional calculus agrees with the canonical identification.

Русский

Отображение, отправляющее тождественную функцию в a через непрерывный функциональный калькулятор, совпадает с канонической идентификацией.

LaTeX

$$continuousFunctionalCalculus_map_id : ...$$

Lean4

theorem cfcHom_eq_of_isStarNormal {A : Type*} [CStarAlgebra A] (a : A) [ha : IsStarNormal a] :
    cfcHom ha = (StarAlgebra.elemental ℂ a).subtype.comp (continuousFunctionalCalculus a) :=
  by
  refine cfcHom_eq_of_continuous_of_map_id ha _ ?_ ?_
  · exact continuous_subtype_val.comp <| (StarAlgEquiv.isometry (continuousFunctionalCalculus a)).continuous
  · simp [continuousFunctionalCalculus_map_id a]

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