English
If the sorted list has at least one element, its first element equals the auxiliary minimum of the Finset.
Русский
Если отсортированный список имеет хотя бы один элемент, его первый элемент равен минимальному в дополнении этой математической структуры.
LaTeX
$$$ (s.sort (\\le)).get \\langle 0, h \\rangle = s.min' H $$$
Lean4
theorem sorted_zero_eq_min'_aux (s : Finset α) (h : 0 < (s.sort (· ≤ ·)).length) (H : s.Nonempty) :
(s.sort (· ≤ ·)).get ⟨0, h⟩ = s.min' H := by
let l := s.sort (· ≤ ·)
apply le_antisymm
· have : s.min' H ∈ l := (Finset.mem_sort (α := α) (· ≤ ·)).mpr (s.min'_mem H)
obtain ⟨i, hi⟩ : ∃ i, l.get i = s.min' H := List.mem_iff_get.1 this
rw [← hi]
exact (s.sort_sorted (· ≤ ·)).rel_get_of_le (Nat.zero_le i)
· have : l.get ⟨0, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l _)
exact s.min'_le _ this
