gauge_sum_le — Mathlib

English

For a finite index set t and f: t → E, gauge s (sum_{i∈t} f(i)) ≤ sum_{i∈t} gauge s (f(i)).

Русский

Для конечного множества индексов t и отображения f: t → E, gauge s(∑ f(i)) ≤ ∑ gauge s(f(i)).

LaTeX

$$$$\\mathrm{gauge}\\!\\left(s, \\sum_{i \\in t} f(i)\\right) \\le \\sum_{i \\in t} \\mathrm{gauge}(s,f(i)).$$$$

Lean4

theorem gauge_sum_le {ι : Type*} (hs : Convex ℝ s) (absorbs : Absorbent ℝ s) (t : Finset ι) (f : ι → E) :
    gauge s (∑ i ∈ t, f i) ≤ ∑ i ∈ t, gauge s (f i) :=
  Finset.le_sum_of_subadditive _ gauge_zero (gauge_add_le hs absorbs) _ _

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