boundedFilterSubmodule — Mathlib

English

The set of functions f with boundedAlong l forms a submodule of α → β.

Русский

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

LaTeX

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

Lean4

/-- The submodule of functions that are bounded along a filter `l`. -/
def boundedFilterSubmodule [SeminormedRing 𝕜] [SeminormedAddCommGroup β] [Module 𝕜 β] [IsBoundedSMul 𝕜 β]
    (l : Filter α) : Submodule 𝕜 (α → β) where
  carrier := BoundedAtFilter l
  zero_mem' := const_boundedAtFilter l 0
  add_mem' hf hg := hf.add hg
  smul_mem' c _ hf := hf.smul c

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