toBoundedContinuousFunctionCLM — Mathlib

English

The Schwartz functions include into the space of bounded continuous maps as a continuous linear map.

Русский

Функции Шварца включаются в пространство ограниченных непрерывных отображений через непрерывное линейное отображение.

LaTeX

$$$$ 𝓢(E,F) \\toL[\\mathbb{C}] E \\to^{\\mathrm{BC}} F. $$$$

Lean4

/-- The inclusion map from Schwartz functions to bounded continuous functions as a continuous linear
map. -/
def toBoundedContinuousFunctionCLM : 𝓢(E, F) →L[𝕜] E →ᵇ F :=
  mkCLMtoNormedSpace toBoundedContinuousFunction (by intro f g; ext; exact add_apply)
    (by intro a f; ext; exact smul_apply)
    (⟨{0}, 1, zero_le_one, by simpa [BoundedContinuousFunction.norm_le (apply_nonneg _ _)] using norm_le_seminorm 𝕜⟩)

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