instMonoid — Mathlib

English

If R is a Monoid with a bounded and continuous multiplication, then the set of bounded continuous functions α →ᵇ R forms a Monoid under the pointwise product (fg)(x) = f(x)g(x).

Русский

Если R - моноид с ограниченным и непрерывным умножением, то множество ограниченных непрерывных функций α →ᵇ R образует моноид относительно покоординатного произведения (fg)(x) = f(x)g(x).

LaTeX

$$$(\alpha \to^{\mathrm{b}} R)$ is a Monoid with multiplication defined by (f \cdot g)(x) = f(x)g(x)$$$

Lean4

@[to_additive]
instance instMonoid [Monoid R] [BoundedMul R] [ContinuousMul R] : Monoid (α →ᵇ R) :=
  Injective.monoid _ DFunLike.coe_injective' rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

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