Commit 2024-08-20 21:56 ddec2bcc

View on Github →

feat: interactions between List.map and sorting lists (#15952) If the function preserves the relation on the list, then the sorting algorithms are unaffected.

Estimated changes

Modified Mathlib/Data/List/Sort.lean

added theorem List.length_insertionSort

added theorem List.map_insertionSort

added theorem List.map_merge

added theorem List.map_mergeSort

added theorem List.map_orderedInsert

added theorem List.map_split

added theorem List.mem_insertionSort

added theorem List.mem_mergeSort

added theorem List.mem_split_iff

Modified Mathlib/Data/Multiset/Sort.lean

added theorem Multiset.map_sort