sorted_last_eq_max' — Mathlib

English

The last element of the sorted list equals the maximum of the Finset.

Русский

Последний элемент отсортированного списка равен максимуму множества.

LaTeX

$$$ (s.sort (\\le))[(s.sort (\\le)).length - 1] = s.max' H $$$

Lean4

theorem sorted_last_eq_max' {s : Finset α} {h : (s.sort (· ≤ ·)).length - 1 < (s.sort (· ≤ ·)).length} :
    (s.sort (· ≤ ·))[(s.sort (· ≤ ·)).length - 1] =
      s.max' (by rw [length_sort] at h; exact card_pos.1 (lt_of_le_of_lt bot_le h)) :=
  sorted_last_eq_max'_aux _ h _

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