instSub — Mathlib

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⟩⟩

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