nnnorm_prod_le — Mathlib

English

For a subalgebra with a norm, the nn-norm of the product is bounded by the product of nn-norms of the factors.

Русский

Для подпалгебры нормирование по nn-norm не превышает произведение nn-norm элементов.

LaTeX

$$$\mathrm{nnnorm}\left(\prod_{i\in s} f(i)\right) \le \prod_{i\in s} \mathrm{nnnorm}(f(i)).$$$

Lean4

theorem nnnorm_prod_le {α : Type*} [NormedCommRing α] [NormOneClass α] (s : Finset ι) (f : ι → α) :
    ‖∏ i ∈ s, f i‖₊ ≤ ∏ i ∈ s, ‖f i‖₊ :=
  (s.norm_prod_le f).trans_eq <| by simp [NNReal.coe_prod]

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