length_insertionSort — Mathlib

English

Sorting by insertionSort preserves length: the length of insertionSort(r,l) equals the length of l.

Русский

Сортировка вставками сохраняет длину: длина insertionSort(r,l) равна длине l.

LaTeX

$$$$ \operatorname{length}(\mathrm{insertionSort}(r,l)) = \operatorname{length}(l). $$$$

Lean4

@[simp]
theorem length_insertionSort (l : List α) : (insertionSort r l).length = l.length :=
  (perm_insertionSort r _).length_eq

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