mergeSort_eq_self

Mathlib.Data.List.Sort

URI: https://scilib.ai/kg/mathlib#List.mergeSort_eq_self

English

If l is sorted with respect to r, then mergeSort l equals l.

Русский

Если список l отсортирован относительно r, то mergeSort l равно l.

LaTeX

$$$ Sorted_r(l) \\Rightarrow mergeSort(l) = l $$$

Lean4

theorem mergeSort_eq_self {l : List α} : Sorted r l → mergeSort l (r · ·) = l :=
  eq_of_perm_of_sorted (mergeSort_perm _ _) (sorted_mergeSort' _ l)

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

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

Разделы

Аффилиация

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