English
Schwartz maps induce a zero-at-infinity bounded continuous function; the underlying bounded continuous function coincides with the zero-at-infinity realization.
Русский
Отображения Шварца порождают ограниченную непрерывную функцию, исчезающую в бесконечности; соответствующая BCФ совпадает с нулевым при бесконечности представлением.
LaTeX
$$$$ f \\mapsto f_{\\mathrm{toBCF}}(x) = f(x). $$$$
Lean4
/-- Schwartz functions as continuous functions vanishing at infinity. -/
def toZeroAtInfty (f : 𝓢(E, F)) : C₀(E, F) where
toFun := f
zero_at_infty' := zero_at_infty f