instAddMonoidOfContinuousAdd — Mathlib

English

If β has an AddMonoid structure with ContinuousAdd, then C_c(α,β) inherits an AddMonoid structure via pointwise addition.

Русский

Если β имеет структуру AddMonoid с ContinuousAdd, тогда C_c(α,β) наследует AddMonoid через сложение по точкам.

LaTeX

$$$$ (f+g)(x) = f(x) + g(x) \quad \text{and} \quad (f+g)\in C_c(\alpha,\beta) $$$$

Lean4

instance [AddMonoid β] [ContinuousAdd β] : AddMonoid C_c(α, β) :=
  DFunLike.coe_injective.addMonoid _ coe_zero coe_add fun _ _ => rfl

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