sort_empty

Mathlib.Data.Finset.Sort

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

English

Sorting the empty Finset yields the empty list.

Русский

Сортировка пустого Finset даёт пустой список.

LaTeX

$$$ \\operatorname{sort}_r(\\emptyset) = [] $$$

Lean4

@[simp]
theorem sort_empty : sort r ∅ = [] :=
  Multiset.sort_zero r

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

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

Разделы

Аффилиация

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