sum_le — Mathlib

English

For any absolute value abv between rings R and S, abv(∑ f_i) ≤ ∑ abv(f_i).

Русский

Для любого абсолютного значения abv между кольцами выполняется неравенство: abv(сумма) ≤ сумма abv(слагаемых).

LaTeX

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

Lean4

theorem sum_le [Semiring R] [Semiring S] [PartialOrder S] [IsOrderedRing S] (abv : AbsoluteValue R S) (s : Finset ι)
    (f : ι → R) : abv (∑ i ∈ s, f i) ≤ ∑ i ∈ s, abv (f i) :=
  Finset.le_sum_of_subadditive abv (map_zero _) abv.add_le _ _

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