English
Let M be a commutative group with an ultrametric norm. For any finite nonempty index set s and any function f from the index set to M, if every ‖f(i)‖ ≤ C, then the norm of the product over i in s is at most C.
Русский
Пусть M — коммутативная группа с ультраметрической нормой. Для любого конечного непустого множества индексов s и функции f: s → M, если для каждого i ∈ s выполняется ‖f(i)‖ ≤ C, то ‖∏_{i∈s} f(i)‖ ≤ C.
LaTeX
$$$\\forall s \\in \\mathrm{Finset}\\,\\iota,\\ s \\neq \\varnothing \\Rightarrow \\forall f: \\iota \\to M, \\forall C \\in \\mathbb{R},\\ (\\forall i \\in s, \\|f(i)\\| \\le C) \\Rightarrow \\|\\prod_{i \\in s} f(i)\\| \\le C$$$
Lean4
/-- Generalised ultrametric triangle inequality for nonempty finite products in commutative groups with
an ultrametric norm.
-/
@[to_additive /-- Generalised ultrametric triangle inequality for nonempty finite sums in additive
commutative groups with an ultrametric norm. -/
]
theorem norm_prod_le_of_forall_le_of_nonempty {s : Finset ι} (hs : s.Nonempty) {f : ι → M} {C : ℝ}
(hC : ∀ i ∈ s, ‖f i‖ ≤ C) : ‖∏ i ∈ s, f i‖ ≤ C :=
(hs.norm_prod_le_sup'_norm f).trans (Finset.sup'_le hs _ hC)
