listSum_le — Mathlib

English

For any list l in R, abv(l.sum) ≤ sum of abv applied to each element of l.

Русский

Для любого списка l ∈ R верно abv(sum l) ≤ sum(abv(li)).

LaTeX

$$$\forall l:\ List\;R,\ abv\big(l.sum\big) \le\; (l.map\ abv).sum$$$

Lean4

/-- The triangle inequality for an `AbsoluteValue` applied to a list. -/
theorem listSum_le [AddLeftMono S] (l : List R) : abv l.sum ≤ (l.map abv).sum := by
  induction l with
  | nil => simp
  | cons head tail ih => exact (abv.add_le ..).trans <| add_le_add_left ih (abv head)

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