instMonoidOfContinuousMul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance [Monoid β] [ContinuousMul β] : Monoid C(α, β) :=
  coe_injective.monoid _ coe_one coe_mul coe_pow

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