toBoundedContinuousFunctionCLM_apply

English

The inclusion from Schwartz functions to bounded continuous maps is a continuous linear map (CLM).

Русский

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

LaTeX

$$$$ 𝓢(E,F) \\toL[\\mathbb{k}] C_0(E,F). $$$$

Lean4

@[simp]
theorem toBoundedContinuousFunctionCLM_apply (f : 𝓢(E, F)) (x : E) : toBoundedContinuousFunctionCLM 𝕜 E F f x = f x :=
  rfl

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