instAddOfContinuousAdd — Mathlib

English

If β is an AddZeroClass with ContinuousAdd, then there is a pointwise addition on C_c(α, β) giving a valid additive structure with HasCompactSupport.add preserved.

Русский

Если β — AddZeroClass с ContinuousAdd, то на C_c(α, β) есть сложение по точкам, сохраняющее компактную опору.

LaTeX

$$$ \text{instance } [AddZeroClass β] [ContinuousAdd β] : Add C_c(α, β) $$$

Lean4

instance [AddZeroClass β] [ContinuousAdd β] : Add C_c(α, β) :=
  ⟨fun f g => ⟨f + g, HasCompactSupport.add f.2 g.2⟩⟩

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