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 𝕜⟩)