sorted_zero_eq_min' — Mathlib

English

The first element of the sorted list equals the minimum of the Finset.

Русский

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

LaTeX

$$$ (s.sort (\\le))[0] = s.min' H $$$

Lean4

theorem sorted_zero_eq_min' {s : Finset α} {h : 0 < (s.sort (· ≤ ·)).length} :
    (s.sort (· ≤ ·))[0] = s.min' (card_pos.1 <| by rwa [length_sort] at h) :=
  sorted_zero_eq_min'_aux _ _ _

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