instMulOneClassOfContinuousMul — Mathlib

English

If β is a monoid with ContinuousMul β, then C(α,β) is a Monoid under pointwise multiplication, with identity map x ↦ 1.

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance [MulOneClass β] [ContinuousMul β] : MulOneClass C(α, β) :=
  coe_injective.mulOneClass _ coe_one coe_mul

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