English
The map cfcHom ha is a closed embedding; in particular its underlying function is continuous.
Русский
Гомоморфизм cfcHom ha является вложением с замкнутым образом; в частности он непрерывен как отображение.
LaTeX
$$$IsClosedEmbedding (cfcHom ha)$$$
Lean4
/-- The star algebra homomorphism underlying a instance of the continuous functional calculus;
a version for continuous functions on the spectrum.
In this case, the user must supply the fact that `a` satisfies the predicate `p`, for otherwise it
may be the case that no star algebra homomorphism exists. For instance if `R := ℝ` and `a` is an
element whose spectrum (in `ℂ`) is disjoint from `ℝ`, then `spectrum ℝ a = ∅` and so there can be
no star algebra homomorphism between these spaces.
While `ContinuousFunctionalCalculus` is stated in terms of these homomorphisms, in practice the
user should instead prefer `cfc` over `cfcHom`.
-/
noncomputable def cfcHom : C(spectrum R a, R) →⋆ₐ[R] A :=
(ContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose
