abs_sum_le_sum_abs — Mathlib

English

For an additive group that is ordered in a compatible way, the absolute value of the sum of elements over a multiset is at most the sum of the absolute values of the elements: |∑_{a∈s} a| ≤ ∑_{a∈s} |a|.

Русский

Для упорядоченной аддитивной группы справедливо неравенство треугольника для сумм по мультимножеству: |∑ a| ≤ ∑ |a|.

LaTeX

$$$$\\left|\\sum_{i \\in s} a_i\\right| \\le \\sum_{i \\in s} |a_i|.$$$$

Lean4

theorem abs_sum_le_sum_abs [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {s : Multiset α} :
    |s.sum| ≤ (s.map abs).sum :=
  le_sum_of_subadditive _ abs_zero abs_add_le s

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