toBoundedContinuousFunction — Mathlib

English

Schwartz maps can be regarded as bounded continuous functions; there is a canonical map sending f ∈ 𝓢(E,F) to its bounded continuous function version.

Русский

Отображения Шварца можно рассматривать как ограниченные непрерывные функции; существует каноническое отображение f ∈ 𝓢(E,F) в соответствующую ограниченно непрерывную функцию.

LaTeX

$$$$ \\text{SchwartzMap } E F \\longrightarrow E \\to^{\\mathrm{BC}} F, $$$$

Lean4

/-- Schwartz functions as bounded continuous functions -/
def toBoundedContinuousFunction (f : 𝓢(E, F)) : E →ᵇ F :=
  BoundedContinuousFunction.ofNormedAddCommGroup f (SchwartzMap.continuous f) (SchwartzMap.seminorm ℝ 0 0 f)
    (norm_le_seminorm ℝ f)

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