sort_singleton

Mathlib.Data.Finset.Sort

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

English

Sorting a singleton Finset {a} yields the list [a].

Русский

Сортировка множества из одного элемента {a} даёт список [a].

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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