inftyNormedRing — Mathlib

English

The space of ∞-norm bounded families with values in normed rings carries a normed ring structure with pointwise operations.

Русский

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

LaTeX

$$$\text{NormedRing}(\lp B\infty)\,,$ i.e., with pointwise addition and multiplication.$$

Lean4

instance inftyNormedRing : NormedRing (lp B ∞) :=
  { lp.inftyRing, lp.nonUnitalNormedRing with }

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