mergeSort_eq_insertionSort — Mathlib

English

Under totality, transitivity and antisymmetry of r, for all l we have mergeSort l = insertionSort r l.

Русский

При условии суммарности, транзитивности и антисимметричности r для любого списка l выполняется равенство mergeSort l = insertionSort r l.

LaTeX

$$$ mergeSort(l) = insertionSort(r,l) $$$

Lean4

theorem mergeSort_eq_insertionSort (l : List α) : mergeSort l (r · ·) = insertionSort r l :=
  eq_of_perm_of_sorted ((mergeSort_perm l _).trans (perm_insertionSort r l).symm) (sorted_mergeSort' r l)
    (sorted_insertionSort r l)

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