norm_prod_le_of_forall_le_of_nonneg

English

In the same setting, if C ≥ 0 and every ‖f(i)‖ ≤ C for i in s, then ‖∏ i∈s f(i)‖ ≤ C.

Русский

В той же постановке, если C ≥ 0 и для всех i ∈ s выполняется ‖f(i)‖ ≤ C, то ‖∏_{i∈s} f(i)‖ ≤ C.

LaTeX

$$$0 \\le C \\Rightarrow (\\forall i \\in s, \\|f(i)\\| \\le C) \\Rightarrow \\left\\|\\prod_{i \\in s} f(i)\\right\\| \\le C$$$

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 norm_prod_le_of_forall_le_of_nonneg {s : Finset ι} {f : ι → M} {C : ℝ} (h_nonneg : 0 ≤ C)
    (hC : ∀ i ∈ s, ‖f i‖ ≤ C) : ‖∏ i ∈ s, f i‖ ≤ C :=
  by
  lift C to NNReal using h_nonneg
  exact nnnorm_prod_le_of_forall_le hC

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