English
In a nonempty finite set, there exists an index i attaining a maximum value of f on the set.
Русский
В ненулевом конечном множестве существует элемент i, достигающий максимума функции f на множестве.
LaTeX
$$$\\\\forall f \\\\ (f : ι → α) \\\\forall s \\\\ (s : Finset ι), s.Nonempty \\\\rightarrow \\\\exists i, MaximalFor (\\\\cdot \\\\in s) f i$$$
Lean4
theorem exists_maximalFor (f : ι → α) (s : Finset ι) (hs : s.Nonempty) : ∃ i, MaximalFor (· ∈ s) f i := by
induction hs using Finset.Nonempty.cons_induction with
| singleton i => exact ⟨i, by simp⟩
| @cons i s hi hs ih =>
obtain ⟨j, hj⟩ := ih
by_cases hji : f j ≤ f i
· refine ⟨i, mem_cons_self .., ?_⟩
simp only [mem_cons, forall_eq_or_imp, imp_self, true_and]
exact fun k hk hik ↦ _root_.trans (hj.2 hk <| _root_.trans hji hik) hji
· exact ⟨j, mem_cons_of_mem hj.1, by simpa [hji] using hj.2⟩
