English
If α is locally compact, β has a multiplication and continuous multiplication, then the pointwise product of continuous maps C(α, β) is a continuous operation, making C(α, β) into a monoid with respect to multiplication whose multiplication is continuous.
Русский
Если α локально компактно, β обладает умножением и непрерывное умножение, то точечное произведение двух непрерывных отображений задаёт непрерывную операцию, превращая C(α, β) в моиду по умножению с непрерывной умножением.
LaTeX
$$$\text{ContinuousMul}(C(\alpha, \beta))\;\text{when } [\text{LocallyCompactSpace } \alpha], [\text{Mul } \beta], [\text{ContinuousMul } \beta]$$$
Lean4
@[to_additive]
instance [LocallyCompactSpace α] [Mul β] [ContinuousMul β] : ContinuousMul C(α, β) :=
⟨by
refine continuous_of_continuous_uncurry _ ?_
have h1 : Continuous fun x : (C(α, β) × C(α, β)) × α => x.fst.fst x.snd :=
continuous_eval.comp (continuous_fst.prodMap continuous_id)
have h2 : Continuous fun x : (C(α, β) × C(α, β)) × α => x.fst.snd x.snd :=
continuous_eval.comp (continuous_snd.prodMap continuous_id)
exact h1.mul h2⟩
