continuousFunctionalCalculus_map_id

English

The continuous functional calculus sends the restricted identity function to the element a.

Русский

Неравно-спектральное отображение непрерывного функционального калькулятора отправляет ограниченную на спектр идентичность в элемент a.

LaTeX

$$continuousFunctionalCalculus a ((ContinuousMap.id ℂ).restrict (spectrum ℂ a)) = ⟨a, self_mem ℂ a⟩$$

Lean4

theorem continuousFunctionalCalculus_map_id :
    continuousFunctionalCalculus a ((ContinuousMap.id ℂ).restrict (spectrum ℂ a)) = ⟨a, self_mem ℂ a⟩ :=
  (gelfandStarTransform (elemental ℂ a)).symm_apply_apply _

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