instAddCommMonoid — Mathlib

English

The zero-at-infinity maps from α to β form a commutative additive monoid under pointwise addition; the zero map is the additive identity.

Русский

Множество отображений с нулём при бесконечности, из α в β, образует коммутативный аддитивный моноид относительно покоординатного сложения; нулевая функция является тождественным элементом сложения.

LaTeX

$$$\C_0(\alpha, \beta)$ forms an AddCommMonoid under pointwise addition: (f+g)(x)=f(x)+g(x), (0)(x)=0.$$$

Lean4

instance instAddCommMonoid [AddCommMonoid β] [ContinuousAdd β] : AddCommMonoid C₀(α, β) :=
  DFunLike.coe_injective.addCommMonoid _ coe_zero coe_add fun _ _ => rfl

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