instNormedRing — Mathlib

English

If R is a NormedRing, then the space α →ᵇ R of bounded continuous functions from α to R carries a NormedRing structure (with pointwise operations).

Русский

Если R — нормированное кольцо, то множество ограниченных непрерывных функций α →ᵇ R может быть наделено структурой нормированного кольца с покоординатными операциями.

LaTeX

$$$\\text{If } [\\text{NormedRing }R] \\text{ then } (\\alpha \\to^b R) \\text{ is a NormedRing}.$$

Lean4

instance instNormedRing [NormedRing R] : NormedRing (α →ᵇ R)
    where
  __ := instRing
  __ := instNonUnitalNormedRing

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