boundedFilterSubalgebra — Mathlib

English

The bounded functions along l form a subalgebra of α → β.

Русский

Ограниченные вдоль l функции образуют подалгебру над основанием.

LaTeX

$$$\\text{boundedFilterSubalgebra}(l) = \\text{Subalgebra}(\\alpha \\to \\beta)$$$

Lean4

/-- The subalgebra of functions that are bounded along a filter `l`. -/
def boundedFilterSubalgebra [SeminormedCommRing 𝕜] [SeminormedRing β] [Algebra 𝕜 β] [IsBoundedSMul 𝕜 β] (l : Filter α) :
    Subalgebra 𝕜 (α → β) :=
  Submodule.toSubalgebra (boundedFilterSubmodule 𝕜 l) (const_boundedAtFilter l (1 : β))
    (fun f g hf hg ↦ by simpa only [Pi.one_apply, mul_one, norm_mul] using hf.mul hg)

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