cfcHom_continuous

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

URI: https://scilib.ai/kg/mathlib#cfcHom_continuous

English

For f ∈ C(spectrum R a, R), the spectrum of cfcHom ha f equals the range of f.

Русский

Для f из C(спектр(a), R) спектр элемента cfcHom ha f равен образу f.

LaTeX

$$spectrum(R, cfcHom ha f) = Set.range f$$

Lean4

@[fun_prop]
theorem cfcHom_continuous : Continuous (cfcHom ha : C(spectrum R a, R) →⋆ₐ[R] A) :=
  cfcHom_isClosedEmbedding ha |>.continuous

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

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

Разделы

Аффилиация

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