sort_perm_toList

Mathlib.Data.Finset.Sort

URI: https://scilib.ai/kg/mathlib#Finset.sort_perm_toList

English

The sorted list of a Finset s is a permutation of the list s.toList.

Русский

Отсортированный список Finset s является перестановкой списка s.toList.

LaTeX

$$$ \\operatorname{sort}_r s \\sim s.toList $$$

Lean4

theorem sort_perm_toList (s : Finset α) : sort r s ~ s.toList :=
  by
  rw [← Multiset.coe_eq_coe]
  simp only [coe_toList, sort_eq]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru