instZeroAtInftyContinuousMapClass

English

The class of compactly supported maps is closed under the ZeroAtInfty property: for every f ∈ F, zero_at_infty f holds by HasCompactSupport is_zero_at_infty (hasCompactSupport f).

Русский

Класс компактно поддерживаемых отображений сохраняет свойство нуля на бесконечности: для каждого f выполнено zero_at_infty f по HasCompactSupport.is_zero_at_infty (hasCompactSupport f).

LaTeX

$$$$ \text{ZeroAtInftyContinuousMapClass } F β γ, \text{ с } zero\_at\_infty f := HasCompactSupport.is\_zero\_at\_infty (hasCompactSupport f). $$$$

Lean4

instance : ZeroAtInftyContinuousMapClass F β γ where
  zero_at_infty f := HasCompactSupport.is_zero_at_infty (hasCompactSupport f)

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