English
A Schwartz map supports subtraction; f - g is again a Schwartz map with subtracted coefficients.
Русский
SchwartzMap поддерживает вычитание; f − g — снова SchwartzMap с вычитанием значений.
LaTeX
$$$ (f - g) \\in 𝓢(E,F) $ if $f,g \\in 𝓢(E,F)$$$
Lean4
instance instSub : Sub 𝓢(E, F) :=
⟨fun f g =>
⟨f - g, (f.smooth _).sub (g.smooth _), by
intro k n
refine ⟨f.seminormAux k n + g.seminormAux k n, fun x => ?_⟩
grw [← f.le_seminormAux k n x, ← g.le_seminormAux k n x]
rw [sub_eq_add_neg]
rw [← decay_neg_aux k n g x]
exact decay_add_le_aux k n f (-g) x⟩⟩