nat_abs_sum_le — Mathlib

English

For a finite set s and a function f: ι → Z, the natAbs of the sum is bounded by the sum of natAbs: |(∑ i∈s f(i))| ≤ ∑ i∈s |f(i)|.

Русский

Для конечного множества s и функции f: ι → Z, неотрицательная абсолютная величина суммы не превышает сумму неотрицательных абсолютных величин: |∑ f(i)| ≤ ∑ |f(i)|.

LaTeX

$$$$ \\left| \\sum_{i \\in s} f(i) \\right| \\le \\sum_{i \\in s} |f(i)|. $$$$

Lean4

theorem nat_abs_sum_le (s : Finset ι) (f : ι → ℤ) : (∑ i ∈ s, f i).natAbs ≤ ∑ i ∈ s, (f i).natAbs := by
  induction s using Finset.cons_induction with grind

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