English
Let a satisfy p(a) and g:R→R be arbitrary. For f a function on the spectrum, viewed as a continuous function in the appropriate sense, the functional calculus on f equals the cfcHom applied to the extension of f along the inclusion, i.e., cfcHom ha f = cfc (Function.extend Subtype.val f g) a.
Русский
Пусть a удовлетворяет p(a). Тогда cfcHom ha f = cfc(Function.extend Subtype.val f g) a для f на спектре, согласно расширению по включению.
LaTeX
$$$ cfcHom ha f = cfc (Function.extend Subtype.val f g) a $$$
Lean4
theorem cfcHom_eq_cfc_extend {a : A} (g : R → R) (ha : p a) (f : C(spectrum R a, R)) :
cfcHom ha f = cfc (Function.extend Subtype.val f g) a :=
by
have h : f = (spectrum R a).restrict (Function.extend Subtype.val f g) := by ext; simp
have hg : ContinuousOn (Function.extend Subtype.val f g) (spectrum R a) :=
continuousOn_iff_continuous_restrict.mpr <| h ▸ map_continuous f
rw [cfc_apply ..]
congr!
