sorted_insertionSort — Mathlib

English

Let r be a relation on α that is total and transitive, and assume is decidable. For any list l, the result of insertionSort r l is a sorted list with respect to r.

Русский

Пусть r — отношение на α, являющееся общим и транзитивным; допустимы решения. Для любого списка l результат сортировки вставками r, то есть insertionSort r l, упорядочен относительно r.

LaTeX

$$$ \\forall l,\\ Sorted r\\ (insertionSort\\ r\\ l) $$$

Lean4

/-- The list `List.insertionSort r l` is `List.Sorted` with respect to `r`. -/
theorem sorted_insertionSort : ∀ l, Sorted r (insertionSort r l)
  | [] => sorted_nil
  | a :: l => (sorted_insertionSort l).orderedInsert a _

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