English
Let t be a finite set of indices and f: indices → M. There exists i ∈ indices such that if t is nonempty then i ∈ t, and ‖∏ j∈t f(j)‖ ≤ ‖f(i)‖.
Русский
Пусть t — конечное множество индексов и f: индексы → M. Существуeт i ∈ индексы такое, что если t непусто, то i ∈ t, и ‖∏_{j∈t} f(j)‖ ≤ ‖f(i)‖.
LaTeX
$$$\\exists i : ι,\\ (t.Nonempty \\Rightarrow i \\in t) \\land \\left\\|\\prod_{j \\in t} f(j)\\right\\| \\le \\|f(i)\\|$$$
Lean4
/-- Given a function `f : ι → M` and a finite set `t ⊆ ι`, we can always find `i : ι`, belonging to `t`
if `t` is nonempty, such that `‖∏ j ∈ t, f j‖ ≤ ‖f i‖`.
-/
@[to_additive /-- Given a function `f : ι → M` and a finite set `t ⊆ ι`, we can always find `i : ι`,
belonging to `t` if `t` is nonempty, such that `‖∑ j ∈ t, f j‖ ≤ ‖f i‖`. -/
]
theorem exists_norm_finset_prod_le (t : Finset ι) [Nonempty ι] (f : ι → M) :
∃ i : ι, (t.Nonempty → i ∈ t) ∧ ‖∏ j ∈ t, f j‖ ≤ ‖f i‖ :=
by
rcases t.eq_empty_or_nonempty with rfl | ht
· simp
exact (fun ⟨i, h, h'⟩ => ⟨i, fun _ ↦ h, h'⟩) <| exists_norm_finset_prod_le_of_nonempty ht f
