instAdd — Mathlib

English

Schwartz maps form an additive group under pointwise addition.

Русский

SchwartzMap образуют аддитивную группу при по точечному сложению.

LaTeX

$$$ (f+g) \\in 𝓢(E,F) $ if $f,g \\in 𝓢(E,F)$$$

Lean4

instance instAdd : Add 𝓢(E, F) :=
  ⟨fun f g =>
    ⟨f + g, (f.smooth _).add (g.smooth _), fun k n =>
      ⟨f.seminormAux k n + g.seminormAux k n, fun x =>
        (decay_add_le_aux k n f g x).trans (add_le_add (f.le_seminormAux k n x) (g.le_seminormAux k n x))⟩⟩⟩

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