cfcₙ_eq_cfcₙL — Mathlib

English

cfcₙ f a equals cfcₙHom ha applied to mkD of the restricted f.

Русский

cfcₙ f a равно применению cfcₙHom ha к mkD ограниченного f.

LaTeX

$$$cfc_n f a = cfc_nHom ha (ContinuousMapZero.mkD ((quasispectrum R a).restrict f) 0)$$$

Lean4

theorem cfcₙ_eq_cfcₙL {a : A} {f : R → R} (ha : p a) (hf : ContinuousOn f (σₙ R a)) (hf0 : f 0 = 0) :
    cfcₙ f a = cfcₙL ha ⟨⟨_, hf.restrict⟩, hf0⟩ := by rw [cfcₙ_def, dif_pos ⟨ha, hf, hf0⟩, cfcₙL_apply]

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