instSemigroupOfContinuousMul — Mathlib

English

Let α, β be topological spaces with β a semigroup and ContinuousMul β. Then the set C(α,β) forms a semigroup under pointwise multiplication, with (f·g)(x) = f(x)·g(x).

Русский

Пусть α, β — топологические пространства, β — полугруппа с непрерывной умножением. Тогда C(α,β) образует полугруппу под точечным умножением: (f·g)(x) = f(x)·g(x).

LaTeX

$$$\forall f,g:\ C(\alpha,\beta): (f\cdot g)(x) = f(x)\cdot g(x) \text{ для всех } x \in \alpha.$$$

Lean4

@[to_additive]
instance [Semigroup β] [ContinuousMul β] : Semigroup C(α, β) :=
  coe_injective.semigroup _ coe_mul

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