instCommMonoid — Mathlib

English

If R is a Commutative Monoid with bounded and continuous multiplication, then the bounded continuous functions α →ᵇ R form a CommMonoid under pointwise multiplication.

Русский

Если R — коммутативный моноид с ограниченным и непрерывным умножением, то ограниченные непрерывные функции α →ᵇ R образуют коммутативный моноид при покоординатном умножении.

LaTeX

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

Lean4

@[to_additive]
instance instCommMonoid [CommMonoid R] [BoundedMul R] [ContinuousMul R] : CommMonoid (α →ᵇ R)
    where
  __ := instMonoid
  mul_comm f g := by ext x; simp [mul_apply, mul_comm]

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