English
If β is a nonunital normed star ring with a C*-ring structure, then for every topological space α, the space C0(α, β) of continuous functions from α to β that vanish at infinity carries a C*-ring structure (i.e., is a C*-algebra without unit).
Русский
Если β — неполностью унитарное нормированное кольцо с операцией звёздочки и структурой C*-кольца, то для любой топологической области α множество C0(α, β) непрерывных функций α → β, которые исчезают в бесконечности, образует C*-кольцо (без единицы).
LaTeX
$$$([NonUnitalNormedRing\,β] \\land [StarRing\,β] \\land [CStarRing\,β]) \\Rightarrow C_0(\\alpha, β) \\text{ является } C^*\\text{-кольцом}$$$
Lean4
instance instCStarRing [NonUnitalNormedRing β] [StarRing β] [CStarRing β] : CStarRing C₀(α, β) where
norm_mul_self_le f := CStarRing.norm_mul_self_le (x := f.toBCF)
