abs_sum_of_nonneg — Mathlib

English

Same as Abs Sum Nonneg Bound: the absolute value of the sum over s is the sum of the absolute values when all terms are nonnegative.

Русский

Аналогично: при неотрицательности слагаемых |∑ f(i)| = ∑ |f(i)|.

LaTeX

$$$ \\forall s : \\mathrm{Finset} \\iota, f : \\iota \\to G\\, [\\text{AddCommGroup } G] [\\text{LinearOrder } G] [\\text{IsOrderedAddMonoid } G], ( \\forall i \\in s, 0 \\le f(i) ) \\Rightarrow |\\sum_{i \\in s} f(i)| = \\sum_{i \\in s} |f(i)|. $$$

Lean4

theorem abs_sum_of_nonneg {G : Type*} [AddCommGroup G] [LinearOrder G] [AddLeftMono G] {f : ι → G} {s : Finset ι}
    (hf : ∀ i ∈ s, 0 ≤ f i) : |∑ i ∈ s, f i| = ∑ i ∈ s, f i := by rw [abs_of_nonneg (Finset.sum_nonneg hf)]

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