English
Let α be a compact space and R a (nonunital) normed ring. Then the set C(α, R) of all continuous maps α → R carries a natural structure of a NonUnitalNormedRing under pointwise addition and multiplication, with the norm given by the supremum of the norms on α.
Русский
Пусть α - компактное множество и R - ненульное нормированное кольцо; тогда множество C(α, R) непрерывных отображений α → R образует ненулевое нормированное кол-во без единицы, имеющее поэлементно сложение и умножение, норму задана как супремум норм отображений.
LaTeX
$$$C(\alpha, R)$ является ненулевым нормированным кольцом без единицы, причем для всех $f,g: \alpha \to R$ и $x\in\alpha$ выполняется $(f+g)(x)=f(x)+g(x)$, $(fg)(x)=f(x)g(x)$ и $\|f\|=\sup_{x\in\alpha}\|f(x)\|$.$$
Lean4
instance [NonUnitalNormedRing R] : NonUnitalNormedRing C(α, R)
where
__ : NormedAddCommGroup C(α, R) := inferInstance
__ : NonUnitalSeminormedRing C(α, R) := inferInstance
