seminormAux_add_le — Mathlib

English

The seminorm of the sum is bounded by the sum of seminorms (second bound).

Русский

Неравенство для суммы seminorm: seminormAux_{k,n}(f+g) ≤ seminormAux_{k,n}(f) + seminormAux_{k,n}(g).

LaTeX

$$$ (f+g).seminormAux_{k,n} \\le f.seminormAux_{k,n} + g.seminormAux_{k,n} $$$

Lean4

theorem seminormAux_add_le (k n : ℕ) (f g : 𝓢(E, F)) :
    (f + g).seminormAux k n ≤ f.seminormAux k n + g.seminormAux k n :=
  (f + g).seminormAux_le_bound k n (add_nonneg (seminormAux_nonneg _ _ _) (seminormAux_nonneg _ _ _)) 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)

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