zeroAtFilterAddSubmonoid — Mathlib

English

The zero-at-filter functions form an additive submonoid of the function space.

Русский

Функции, сходящиеся к нулю вдоль л, образуют добавочно-подмножество в пространстве функций.

LaTeX

$$$\\{ f : \\alpha \\to β \\mid \\mathrm{ZeroAtFilter}(l,f) \\} \\text{ is an additive submonoid of } (\\alpha \\to β)$$$

Lean4

/-- `zeroAtFilterAddSubmonoid l` is the additive submonoid of `f : α → β`
which tend to zero along `l`. -/
def zeroAtFilterAddSubmonoid [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] (l : Filter α) :
    AddSubmonoid (α → β) where
  carrier := ZeroAtFilter l
  add_mem' ha hb := ha.add hb
  zero_mem' := zero_zeroAtFilter l

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