cfcHom_map_spectrum — Mathlib

English

For ha: p a, the image under cfcHom ha of a test function f lies in the predicate p.

Русский

При ha: p a образ cfcHom ha от тестовой функции f удовлетворяет условию предиката p.

LaTeX

$$p (cfcHom ha f)$$

Lean4

/-- The **spectral mapping theorem** for the continuous functional calculus. -/
theorem cfcHom_map_spectrum (f : C(spectrum R a, R)) : spectrum R (cfcHom ha f) = Set.range f :=
  (ContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose_spec.2.2.1 f

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