cfcL — Mathlib

English

The map cfcHom ha can be packaged as a continuous linear map, denoted cfcL ha, from the function space to A, preserving scalars and continuity.

Русский

Отображение cfcHom ha превращают в непрерывно линейное отображение cfcL ha из пространства функций в A, сохраняющее скалярное умножение и непрерывность.

LaTeX

$$$cfcL ha : C(\\mathrm{spectrum}(R,a),R) \\to_L[R] A$$$

Lean4

/-- `cfcHom` bundled as a continuous linear map. -/
@[simps apply]
noncomputable def cfcL {a : A} (ha : p a) : C(spectrum R a, R) →L[R] A :=
  { cfcHom ha with
    toFun := cfcHom ha
    map_smul' := map_smul _
    cont := (cfcHom_isClosedEmbedding ha).continuous }

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