coeToLp — Mathlib

English

There is a natural continuous linear map embedding Lp.simpleFunc into Lp, given by inclusion.

Русский

Существует естественное непрерывное линейное вложение Lp.simpleFunc в Lp, задаваемое включением.

LaTeX

$$$coeToLp : Lp.simpleFunc E p μ \toL[𝕜] Lp E p μ \;\text{ является непрерывным линейным отображением}$$$

Lean4

/-- The embedding of Lp simple functions into Lp functions, as a continuous linear map. -/
def coeToLp : Lp.simpleFunc E p μ →L[𝕜] Lp E p μ :=
  {
    AddSubgroup.subtype (Lp.simpleFunc E p μ) with
    map_smul' := fun _ _ => rfl
    cont := Lp.simpleFunc.uniformContinuous.continuous }

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