norm_prod_le — Mathlib

English

In a product of normed rings, the norm is submultiplicative: ∥ab∥ ≤ ∥a∥∥b∥ for all a,b in the product.

Русский

В произведении нормированных колец норма подмультпликативна: ∥ab∥ ≤ ∥a∥∥b∥.

LaTeX

$$$\forall a,b \in \alpha\times\beta:\ \|ab\| ≤ \|a\|\|b\|.$$$

Lean4

theorem norm_prod_le {α : Type*} [NormedCommRing α] [NormOneClass α] (s : Finset ι) (f : ι → α) :
    ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖ := by
  rcases s with ⟨⟨l⟩, hl⟩
  simpa using (l.map f).norm_prod_le

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