English
For any r in R and any function f: R → R, applying the continuous functional calculus to the algebra-map image of r equals the algebra-map image of f(r).
Русский
Для любого r в R и любой f: R → R применение непрерывного функционального вычисления к образу r под алгебраической вложенной карты равно образу f(r) под той же алгебраической картой.
LaTeX
$$$ cfc\, f\; (\ algebraMap\ R\ A\ r) = \ algebraMap\ R\ A\ (f\, r) $$$
Lean4
@[simp]
theorem cfc_algebraMap (r : R) (f : R → R) : cfc f (algebraMap R A r) = algebraMap R A (f r) :=
by
have h₁ : ContinuousOn f (spectrum R (algebraMap R A r)) :=
continuousOn_singleton _ _ |>.mono <| CFC.spectrum_algebraMap_subset r
rw [cfc_apply f (algebraMap R A r) (cfc_predicate_algebraMap r), ←
AlgHomClass.commutes (cfcHom (p := p) (cfc_predicate_algebraMap r)) (f r)]
congr
ext ⟨x, hx⟩
apply CFC.spectrum_algebraMap_subset r at hx
simp_all
