norm_tprod_le_of_forall_le_of_nonneg

English

If ∀ i, ‖f(i)‖₊ ≤ C, then ‖∏' i, f i‖₊ ≤ C.

Русский

Если для всех i выполняется ‖f(i)‖₊ ≤ C, то ‖∏' i, f i‖₊ ≤ C.

LaTeX

$$$\\forall f : ι \\to M,\\forall C : \\mathbb{R}_{\\ge 0},\\ (\\forall i, \\|f(i)\\|_{+} \\le C) \\Rightarrow \\|\\prod' i, f(i)\\|_{+} \\le C$$$

Lean4

@[to_additive]
theorem norm_tprod_le_of_forall_le_of_nonneg {f : ι → M} {C : ℝ} (hC : 0 ≤ C) (h : ∀ i, ‖f i‖ ≤ C) : ‖∏' i, f i‖ ≤ C :=
  by
  rcases isEmpty_or_nonempty ι
  · simpa only [tprod_empty, norm_one'] using hC
  · exact norm_tprod_le_of_forall_le h

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