toZeroAtInftyCLM — Mathlib

English

There is a continuous linear map from Schwartz functions to zero-at-infinity continuous maps.

Русский

Существует непрерывно-линейное отображение из функций Шварца в нулевые при бесконечности непрерывные отображения.

LaTeX

$$$$ \\text{toZeroAtInftyCLM} : 𝓢(E,F) \\toL[𝕜] C_0(E,F). $$$$

Lean4

/-- The inclusion map from Schwartz functions to continuous functions vanishing at infinity as a
continuous linear map. -/
def toZeroAtInftyCLM : 𝓢(E, F) →L[𝕜] C₀(E, F) :=
  mkCLMtoNormedSpace toZeroAtInfty (by intro f g; ext; exact add_apply) (by intro a f; ext; exact smul_apply)
    (⟨{0}, 1, zero_le_one, by
      simpa [← ZeroAtInftyContinuousMap.norm_toBCF_eq_norm, BoundedContinuousFunction.norm_le (apply_nonneg _ _)] using
        norm_le_seminorm 𝕜⟩)

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