nnnorm_prod_le_of_forall_le — Mathlib

English

If s is nonempty, then the norm of the product is ≤ the sup of norms of factors.

Русский

Если множество непусто, то норма произведения ≤ суп норм факторов.

LaTeX

$$$s.Nonempty \\Rightarrow \\|\\prod_{i\\in s} f(i)\\| ≤ s.sup' (\\|f·\\|)$$$

Lean4

/-- Generalised ultrametric triangle inequality for finite products in commutative groups with
an ultrametric norm.
-/
@[to_additive /-- Generalised ultrametric triangle inequality for finite sums in additive
    commutative groups with an ultrametric norm. -/
    ]
theorem nnnorm_prod_le_of_forall_le {s : Finset ι} {f : ι → M} {C : ℝ≥0} (hC : ∀ i ∈ s, ‖f i‖₊ ≤ C) :
    ‖∏ i ∈ s, f i‖₊ ≤ C :=
  (s.nnnorm_prod_le_sup_nnnorm f).trans <| Finset.sup_le hC

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