norm_prod_le — Mathlib

English

For any nonempty list l of elements in a seminormed ring, the norm of the product is at most the product of the norms.

Русский

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

LaTeX

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

Lean4

theorem norm_prod_le [NormOneClass α] : ∀ l : List α, ‖l.prod‖ ≤ (l.map norm).prod
  | [] => by simp
  | a :: l => List.norm_prod_le' (List.cons_ne_nil a l)

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