instMonoidWithZeroOfContinuousMul

English

If β is a MonoidWithZero with ContinuousMul β, then C(α,β) is a MonoidWithZero under pointwise multiplication.

Русский

Если β — MonoidWithZero с непрерывным умножением, то C(α,β) является MonoidWithZero под точечным умножением.

LaTeX

$$$\forall f,g:\ C(\alpha,\beta): (f\cdot g)(x) = f(x)\cdot g(x),\ 0_{C(\alpha,\beta)}(x)=0_{\beta},\ 1_{C(\alpha,\beta)}(x)=1_{\beta}. $$$

Lean4

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

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