instNormedRing — Mathlib

English

If α is compact and R is a normed ring, then C(α, R) has a NormedRing structure with pointwise operations and the sup-norm.

Русский

Пусть α компактно, а R - нормированное кольцо; тогда C(α, R) образует нормированное кольцо с точечно определяемыми операциями и суп-нормой.

LaTeX

$$$C(\alpha, R)$ is a NormedRing with (f+g)(x)=f(x)+g(x), (fg)(x)=f(x)g(x), and $\|f\|=\sup_{x\in\alpha}\|f(x)\|$.$$

Lean4

instance [NormedRing R] : NormedRing C(α, R)
    where
  __ : NormedAddCommGroup C(α, R) := inferInstance
  __ : SeminormedRing C(α, R) := inferInstance

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