cfc_eq_cfcL — Mathlib

English

If a satisfies p(a) and f is continuous on the spectrum of a, then cfc f a equals the linear functional calculus cfcL applied to the appropriate restriction of f.

Русский

Если a удовлетворяет p(a) и f непрерывна на спектре a, то cfc f a = cfcL ha ⟨ f|_{spectrum(R,a)}, hf.restrict ⟩.

LaTeX

$$$ cfc\, f\, a = cfcL ha \langle (spectrum\, R\, a).restrict\, f, hf.restrict\rangle $$$

Lean4

theorem cfc_eq_cfcL {a : A} {f : R → R} (ha : p a) (hf : ContinuousOn f (spectrum R a)) :
    cfc f a = cfcL ha ⟨_, hf.restrict⟩ := by rw [cfc_def, dif_pos ⟨ha, hf⟩, cfcL_apply]

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