abv_sum — Mathlib

English

More general form: abv(sum f_i) ≤ sum abv(f_i) for an absolute value abv on R to S.

Русский

Обобщенная форма: abv(сумма f_i) ≤ сумма abv(f_i) для абсолютного значения abv на R→S.

LaTeX

$$$\operatorname{abv}\left(\sum_{i\in s} f(i)\right) \le \sum_{i\in s} \operatorname{abv}(f(i))$$$

Lean4

theorem abv_sum [Semiring R] [Semiring S] [PartialOrder S] [IsOrderedRing S] (abv : R → S) [IsAbsoluteValue abv]
    (f : ι → R) (s : Finset ι) : abv (∑ i ∈ s, f i) ≤ ∑ i ∈ s, abv (f i) :=
  (IsAbsoluteValue.toAbsoluteValue abv).sum_le _ _

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