English
For a nonempty Finset s and f: ι → M, the nnNorm of the product is ≤ the sup of nnNorms of factors.
Русский
Для непустого Finset s и отображения f, nnNorm от произведения не больше супа nnNorm от факторов.
LaTeX
$$$s \\neq \\varnothing \\Rightarrow \\|\\prod_{i \\in s} f(i)\\|_+ ≤ s.sup' (\\|f·\\|_+)$$$
Lean4
/-- Nonarchimedean norm of a product is less than or equal to the largest norm of a term in the
product. -/
@[to_additive /-- Nonarchimedean norm of a sum is less than or equal to the largest norm of a term
in the sum. -/
]
theorem _root_.Finset.nnnorm_prod_le_sup_nnnorm (s : Finset ι) (f : ι → M) : ‖∏ i ∈ s, f i‖₊ ≤ s.sup (‖f ·‖₊) :=
by
rcases s.eq_empty_or_nonempty with rfl | hs
· simp only [Finset.prod_empty, nnnorm_one', Finset.sup_empty, bot_eq_zero', le_refl]
· simpa only [← Finset.sup'_eq_sup hs, Finset.le_sup'_iff, coe_le_coe, coe_nnnorm'] using hs.norm_prod_le_sup'_norm f
