cfcₙ_id

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

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

English

If two functions coincide on the spectrum, then their outputs via cfc coincide.

Русский

Если две функции совпадают на спектре, тогда их значения через cfc совпадают.

LaTeX

$$Set.EqOn f g (quasispectrum R a) → cfcₙ f a = cfcₙ g a$$

Lean4

theorem cfcₙ_id : cfcₙ (id : R → R) a = a :=
  cfcₙ_apply (id : R → R) a ▸ cfcₙHom_id (p := p) ha

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

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

Разделы

Аффилиация

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