max'_eq_sorted_last — Mathlib

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

Похожие утверждения