abs_sum_of_nonneg' — Mathlib

English

Variant of Abs Sum Nonneg: same equality when f(i) ≥ 0 for all i.

Русский

Вариант: та же равенство при неотрицательности f(i).

LaTeX

$$$ \\forall s : \\mathrm{Finset} \\iota, f : \\iota \\to G\\, [\\text{AddCommGroup } G] [\\text{LinearOrder } G] [\\text{IsOrderedAddMonoid } G], ( \\forall i, i \\in s \\Rightarrow 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, 0 ≤ f i) : |∑ i ∈ s, f i| = ∑ i ∈ s, f i := by rw [abs_of_nonneg (Finset.sum_nonneg' hf)]

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