toZeroAtInfty — Mathlib

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

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