Commit 2024-09-29 08:52 a6006d2f

View on Github →

feat: stability of List.insertionSort (#16065) The statements of stability follow those used for mergeSort in leanprover/lean4#5092.

Estimated changes

Modified Mathlib/Data/List/Sort.lean

added theorem List.Sublist.orderedInsert_sublist

added theorem List.cons_sublist_orderedInsert

added theorem List.pair_sublist_insertionSort'

added theorem List.pair_sublist_insertionSort

added theorem List.sublist_insertionSort'

added theorem List.sublist_insertionSort