cfcₙ_id'

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

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

English

If f is continuous on the spectrum and f(0)=0, then cfcₙ f a equals cfcₙL ha applied to the restricted f.

Русский

Если f непрерывна на спектре и f(0)=0, то cfcₙ f a равно cfcₙL ha применённому к ограниченному f.

LaTeX

$$cfcₙ f a = cfcₙL ha ⟨⟨_, hf.restrict⟩, hf0⟩$$

Lean4

theorem cfcₙ_id' : cfcₙ (fun x : R ↦ x) a = a :=
  cfcₙ_id R a

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

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

Разделы

Аффилиация

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