cfcₙL — Mathlib

English

The functional calculus is packaged as a continuous linear map cfcₙL with the same action as cfcₙHom.

Русский

Функциональный калькулятор упакован как непрерывно-линейный отображение cfcₙL, с тем же действием, что и cfcₙHom.

LaTeX

$$$\mathrm{cfc}_{nL ha}: C(σ_n R a, R)_0 \to_L A$, with $\mathrm{toFun}=\mathrm{cfc}_nHom ha$$$

Lean4

/-- `cfcₙHom` bundled as a continuous linear map. -/
@[simps apply]
noncomputable def cfcₙL {a : A} (ha : p a) : C(σₙ R a, R)₀ →L[R] A :=
  { cfcₙHom ha with
    toFun := cfcₙHom ha
    map_smul' := map_smul _
    cont := (cfcₙHom_isClosedEmbedding ha).continuous }

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