instCommMonoidWithZeroOfContinuousMul

English

Let α, β be topological spaces with β a commutative monoid with zero and continuous multiplication. Then the set C(α, β) of continuous maps α → β forms a commutative monoid with zero under the pointwise product.

Русский

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

LaTeX

$$$\big(C(\alpha, \beta),\cdot,1,0\big) \\text{with } (f\cdot g)(x)=f(x)g(x),\; (0)(x)=0_{\beta},\; (1)(x)=1_{\beta} \\text{is a commutative monoid with zero}$$$

Lean4

instance [CommMonoidWithZero β] [ContinuousMul β] : CommMonoidWithZero C(α, β) :=
  coe_injective.commMonoidWithZero _ coe_zero coe_one coe_mul coe_pow

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