instCommSemiringOfIsTopologicalSemiring

English

Let α be a topological space and β a topological commutative semiring. Then the set of all continuous maps from α to β, with pointwise addition and multiplication, forms a commutative semiring under these operations.

Русский

Пусть α — топологическое пространство, β — топологическое коммутативное полукольцо. Тогда множество непрерывных отображений α → β с точечными операциями сложения и умножения образует коммутативное полукольцо.

LaTeX

$$$ C(\alpha, \beta) \quad\text{is a}\quad \mathrm{CommSemiring}\, C(\alpha, \beta) \quad\text{with pointwise operations: } (f+g)(x)=f(x)+g(x),\; (f\cdot g)(x)=f(x)\,g(x),\; 0(x)=0,\; 1(x)=1. $$$

Lean4

instance {α : Type*} {β : Type*} [TopologicalSpace α] [TopologicalSpace β] [CommSemiring β] [IsTopologicalSemiring β] :
    CommSemiring C(α, β) :=
  coe_injective.commSemiring _ coe_zero coe_one coe_add coe_mul coe_nsmul coe_pow coe_natCast

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