instMul — Mathlib

English

If β is a monoid with continuous multiplication, then the set of continuous maps C(α, β) forms a monoid under pointwise multiplication.

Русский

Если β является моноидом с непрерывным умножением, то множество непрерывных отображений C(α, β) образует моноид при попиксовом умножении.

LaTeX

$$If [Monoid β] [ContinuousMul β], then Mul (C(α, β)) is defined by (f * g)(x) = f(x) g(x) with identity 1 given by the constant map 1.$$

Lean4

@[to_additive]
instance instMul [Mul β] [ContinuousMul β] : Mul C(α, β) :=
  ⟨fun f g => ⟨f * g, continuous_mul.comp (f.continuous.prodMk g.continuous :)⟩⟩

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