instSemigroupWithZeroOfContinuousMul

English

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

Русский

Если β — полугруппа с нулём и непрерывным умножением, то C(α,β) образует SemigroupWithZero под точечным умножением.

LaTeX

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

Lean4

instance [SemigroupWithZero β] [ContinuousMul β] : SemigroupWithZero C(α, β) :=
  coe_injective.semigroupWithZero _ coe_zero coe_mul

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