pair_sublist_insertionSort — Mathlib

English

If r a b holds and [a,b] is a sublist of l, then [a,b] is a sublist of insertionSort r l.

Русский

Если r a b выполняется и пара [a,b] является подпоследовательностью списка l, то [a,b] является подпоследовательностью к insertionSort r l.

LaTeX

$$$ r\\ a\\ b \\Rightarrow ([a,b] <+ l) \\Rightarrow ([a,b] <+ insertionSort r l) $$$

Lean4

/-- Another statement of stability of insertion sort.
If a pair `[a, b]` is a sublist of `l` and `r a b`,
then `[a, b]` is still a sublist of `insertionSort r l`.
-/
theorem pair_sublist_insertionSort {a b : α} {l : List α} (hab : r a b) (h : [a, b] <+ l) :
    [a, b] <+ insertionSort r l :=
  sublist_insertionSort (pairwise_pair.mpr hab) h

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