nnnorm_multiset_prod_le — Mathlib

English

For any multiset m of elements in a seminormed commutative group, the nonnegative norm of the product is at most the sum of the nonnegative norms of the elements.

Русский

Для любой мультисета элементов в полугруппе с нормой неотрицательное нормирование произведения не превосходит сумму неотрицательных норм элементов.

LaTeX

$$$\displaystyle \|m.\mathrm{prod}\|_+ \le \bigl(m.map(\lambda x. \|x\|_+ )\bigr).\mathrm{sum}$$$

Lean4

@[to_additive]
theorem nnnorm_multiset_prod_le (m : Multiset E) : ‖m.prod‖₊ ≤ (m.map fun x => ‖x‖₊).sum :=
  NNReal.coe_le_coe.1 <| by
    push_cast
    rw [Multiset.map_map]
    exact norm_multiset_prod_le _

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