sort_sorted

Mathlib.Data.Finset.Sort

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

English

Sorting with respect to r yields a List that is sorted by r.

Русский

Сортированный по r список является упорядоченным по отношению r.

LaTeX

$$$ \mathrm{List.Sorted}\, r\, (\mathrm{sort}\, r\, s) $$$

Lean4

@[simp]
theorem sort_sorted (s : Finset α) : List.Sorted r (sort r s) :=
  Multiset.sort_sorted _ _

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

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

Разделы

Аффилиация

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