norm_multiset_prod_le — Mathlib

English

If for each b in a finite set s we have ‖f(b)‖ ≤ n(b), then ‖∏ f(b)‖ ≤ ∑ n(b).

Русский

Если для каждого b в конечном наборе s верно ‖f(b)‖ ≤ n(b), то ‖∏ f(b)‖ ≤ ∑ b∈s n(b).

LaTeX

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

Lean4

@[to_additive existing]
theorem norm_multiset_prod_le (m : Multiset E) : ‖m.prod‖ ≤ (m.map fun x => ‖x‖).sum :=
  by
  rw [← Multiplicative.ofAdd_le, ofAdd_multiset_prod, Multiset.map_map]
  refine Multiset.le_prod_of_submultiplicative (Multiplicative.ofAdd ∘ norm) ?_ (fun x y => ?_) _
  · simp only [comp_apply, norm_one', ofAdd_zero]
  · exact norm_mul_le' x y

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