perm_insertionSort — Mathlib

English

For any l, the sorting by insertionSort is a permutation of l.

Русский

Для любого списка l сортировка вставками образует перестановку списка l.

LaTeX

$$$$ \forall l:\mathrm{List}(\alpha),\; \mathrm{insertionSort}(r,l) \;\sim\; l. $$$$

Lean4

theorem perm_insertionSort : ∀ l : List α, insertionSort r l ~ l
  | [] => Perm.nil
  | b :: l => by simpa [insertionSort] using (perm_orderedInsert _ _ _).trans ((perm_insertionSort l).cons b)

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