norm_prod_le — Mathlib

English

Again, the norm of a finite product is at most the sum of the norms.

Русский

Снова нормa конечного произведения не больше суммы норм.

LaTeX

$$$$\Big\|\prod_{i\in s} f(i)\Big\| \le \sum_{i\in s} \|f(i)\|.$$$$

Lean4

@[to_additive existing]
theorem norm_prod_le (s : Finset ι) (f : ι → E) : ‖∏ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖ :=
  by
  rw [← Multiplicative.ofAdd_le, ofAdd_sum]
  refine Finset.le_prod_of_submultiplicative (Multiplicative.ofAdd ∘ norm) ?_ (fun x y => ?_) _ _
  · simp only [comp_apply, norm_one', ofAdd_zero]
  · exact norm_mul_le' x y

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