English
If β is a ring with a compatible topology (a topological ring), the set C(α, β) of continuous maps α → β carries a natural ring structure given pointwise addition and multiplication: (f+g)(x)=f(x)+g(x), (f·g)(x)=f(x)·g(x).
Русский
Если β — топологическое кольцо, тогда множество C(α, β) непрерывных отображений имеет естественное кольцевое произведение, заданное по точке: (f+g)(x)=f(x)+g(x), (f·g)(x)=f(x)g(x).
LaTeX
$$$ (f+g)(x) = f(x) + g(x), \quad (f\cdot g)(x) = f(x)\,g(x) \quad\text{для всех } x. $$$
Lean4
instance instRing {α : Type*} {β : Type*} [TopologicalSpace α] [TopologicalSpace β] [Ring β] [IsTopologicalRing β] :
Ring C(α, β) :=
coe_injective.ring _ coe_zero coe_one coe_add coe_mul coe_neg coe_sub coe_nsmul coe_zsmul coe_pow coe_natCast
coe_intCast
