zeroAtFilterSubmodule — Mathlib

English

The set of all functions f with ZeroAtFilter(l,f) forms a submodule of the function space α → β.

Русский

Множество всех функций f с ZeroAtFilter(l,f) является подмодулем пространства функций α → β.

LaTeX

$$$\\{ f : \\alpha \\to β \\mid \\mathrm{ZeroAtFilter}(l,f) \\} \\text{ is a submodule of } (\\alpha \\to β)$$$

Lean4

/-- `zeroAtFilterSubmodule l` is the submodule of `f : α → β` which
tend to zero along `l`. -/
def zeroAtFilterSubmodule [TopologicalSpace β] [Semiring 𝕜] [AddCommMonoid β] [Module 𝕜 β] [ContinuousAdd β]
    [ContinuousConstSMul 𝕜 β] (l : Filter α) : Submodule 𝕜 (α → β)
    where
  carrier := ZeroAtFilter l
  zero_mem' := zero_zeroAtFilter l
  add_mem' ha hb := ha.add hb
  smul_mem' c _ hf := hf.smul c

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