sort_toFinset — Mathlib

English

Let s be a Finset. Sorting s and then converting back to a Finset yields s again.

Русский

Пусть S — Finset. Отсортированный по порядку список S затем преобразуется обратно к Finset; полученная Finset равна S.

LaTeX

$$$ (\\operatorname{sort}_r s).toFinset = s $$$

Lean4

@[simp]
theorem sort_toFinset [DecidableEq α] (s : Finset α) : (sort r s).toFinset = s :=
  List.toFinset_eq (sort_nodup r s) ▸ eq_of_veq (sort_eq r s)

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