English
The maximum of a nonempty Finset equals the last element of its sorted list.
Русский
Максимум не пустого Finset равен последнему элементу отсортированного списка.
LaTeX
$$$ s.max' H = (s.sort (\\le))[(s.sort (\\le)).length - 1] $$$
Lean4
theorem max'_eq_sorted_last {s : Finset α} {h : s.Nonempty} :
s.max' h =
(s.sort (· ≤ ·))[(s.sort (· ≤ ·)).length - 1]'(by simpa using Nat.sub_lt (card_pos.mpr h) Nat.zero_lt_one) :=
(sorted_last_eq_max'_aux _ (by simpa using Nat.sub_lt (card_pos.mpr h) Nat.zero_lt_one) _).symm