cfcₙ_eq_cfcₙL_mkD — Mathlib

English

Applying cfcₙHom to f and then taking a suitable extension recovers the same as applying cfc to the extended f.

Русский

Применение cfcₙHom к f с последующим расширением восстанавливает то же самое, что применение cfc к расширенному f.

LaTeX

$$cfcₙHom ha f = cfcₙ (Function.extend Subtype.val (ContinuousMapZero.instFunLike.coe f) g) a$$

Lean4

/-- A version of `cfcₙ_eq_cfcₙL` in terms of `ContinuousMapZero.mkD` -/
theorem cfcₙ_eq_cfcₙL_mkD : cfcₙ f a = cfcₙL (a := a) ha (mkD ((quasispectrum R a).restrict f) 0) :=
  cfcₙ_apply_mkD _ _

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