cfc_eq_cfcL_mkD — Mathlib

English

Equivalently, cfc f a equals cfcL ha (mkD((spectrum R a).restrict f) 0). This ties the L-implementation to the mkD formulation.

Русский

Справедливо равенство cfc f a = cfcL ha (mkD((spectrum R a).restrict f) 0).

LaTeX

$$$ cfc f a = cfcL (a) ha (mkD ((spectrum R a).restrict f) 0) $$$

Lean4

/-- A version of `cfc_eq_cfcL` in terms of `ContinuousMapZero.mkD` -/
theorem cfc_eq_cfcL_mkD : cfc f a = cfcL (a := a) ha (mkD ((spectrum R a).restrict f) 0) :=
  cfc_apply_mkD _ _

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