English
Let t be a nonempty finite set of indices and f: indices → M. There exists an index i ∈ indices such that the norm of the product over t is bounded by ‖f(i)‖.
Русский
Пусть t — непустое конечное множество индексов, и дано отображение f: индексы → M. Всегда существует элемент i ∈ t такой, что ‖∏_{j∈t} f(j)‖ ≤ ‖f(i)‖.
LaTeX
$$$\\forall t \\in \\mathrm{Finset}\\,\\iota,\\ t'.Nonempty \\Rightarrow \\exists i \\in t,\\ \\left\\|\\prod_{j \\in t} f(j)\\right\\| \\le \\|f(i)\\|$$$
Lean4
/-- Given a function `f : ι → M` and a nonempty finite set `t ⊆ ι`, we can always find `i ∈ t` such that
`‖∏ j in t, f j‖ ≤ ‖f i‖`.
-/
@[to_additive /-- Given a function `f : ι → M` and a nonempty finite set `t ⊆ ι`, we can always find
`i ∈ t` such that `‖∑ j ∈ t, f j‖ ≤ ‖f i‖`. -/
]
theorem exists_norm_finset_prod_le_of_nonempty {t : Finset ι} (ht : t.Nonempty) (f : ι → M) :
∃ i ∈ t, ‖∏ j ∈ t, f j‖ ≤ ‖f i‖ :=
match t.exists_mem_eq_sup' ht (‖f ·‖) with
| ⟨j, hj, hj'⟩ => ⟨j, hj, (ht.norm_prod_le_sup'_norm f).trans (le_of_eq hj')⟩
