nnnorm_prod_le — Mathlib

English

For a finite index set s and function f: s → E, the norm of the product ∏_{a∈s} f(a) is at most the sum of the norms of f(a).

Русский

Для конечного множества индексов s и функции f: s→E нормa произведения не превосходит сумму норм f(a).

LaTeX

$$$\displaystyle \|\prod_{a\in s} f(a)\| \le \sum_{a\in s} \|f(a)\|$$$

Lean4

@[to_additive]
theorem nnnorm_prod_le (s : Finset ι) (f : ι → E) : ‖∏ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊ :=
  NNReal.coe_le_coe.1 <| by
    push_cast
    exact norm_prod_le _ _

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