sort_singleton

Mathlib.Data.Multiset.Sort

URI: https://scilib.ai/kg/mathlib#Multiset.sort_singleton

English

Sorting a singleton multiset yields a singleton list.

Русский

Сортировка одиночного мультисета дает единичный список.

LaTeX

$$$$ \\operatorname{sort} r \\{a\\} = [a] $$$$

Lean4

@[simp]
theorem sort_singleton (a : α) : sort r { a } = [a] :=
  List.mergeSort_singleton a

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

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

Разделы

Аффилиация

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