English
For an additive group with a linear order in which addition is order-preserving, the absolute value of the sum over s is at most the sum of the absolute values: |∑_{i∈s} f(i)| ≤ ∑_{i∈s} |f(i)| when f(i) are nonnegative.
Русский
В упорядоченной абелевой группе с сохранением порядка сложения выполняется неравенство модуля суммы: |∑_{i∈s} f(i)| ≤ ∑_{i∈s} |f(i)|, когда f(i) неотрицательны.
LaTeX
$$$ \\forall s : \\mathrm{Finset} \\iota, f : \\iota \\to G\\, [\\text{AddCommGroup } G] [\\text{LinearOrder } G] [\\text{IsOrderedAddMonoid } G], \\left( \\forall i \\in s, 0 \\le f(i) \\right) \\Rightarrow \\left| \\sum_{i \\in s} f(i) \\right| \\le \\sum_{i \\in s} |f(i)|. $$$
Lean4
theorem abs_sum_le_sum_abs {G : Type*} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (f : ι → G)
(s : Finset ι) : |∑ i ∈ s, f i| ≤ ∑ i ∈ s, |f i| :=
le_sum_of_subadditive _ abs_zero abs_add_le s f
