nnnorm_prod_le — Mathlib

English

If l is a nonempty list, then the nonnegative norm of the product is at most the product of the nonnegative norms.

Русский

Если список непустой, то nnnorm произведения не превосходит произведения nnnorm отдельных элементов.

LaTeX

$$$\|\prod_{i \in l} f(i)\|_{\!}\! \le \prod_{i \in l} \|f(i)\|_{\!}. $$$

Lean4

theorem nnnorm_prod_le [NormOneClass α] (l : List α) : ‖l.prod‖₊ ≤ (l.map nnnorm).prod :=
  l.norm_prod_le.trans_eq <| by simp [NNReal.coe_list_prod, List.map_map]

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