Commit 2023-01-18 10:14 9bff38a4

View on Github →

feat: port Data.List.Sort (#1632)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/Sort.lean

added theorem List.Monotone.ofFn_sorted

added theorem List.Sorted.insertionSort_eq

added theorem List.Sorted.merge

added theorem List.Sorted.of_cons

added theorem List.Sorted.orderedInsert

added theorem List.Sorted.rel_nthLe_of_le

added theorem List.Sorted.rel_nthLe_of_lt

added theorem List.Sorted.rel_of_mem_take_of_mem_drop

added theorem List.Sorted.tail

added def List.Sorted

added theorem List.eq_of_perm_of_sorted

added def List.insertionSort

added theorem List.insertionSort_cons_eq_take_drop

added theorem List.length_mergeSort

added theorem List.length_split_le

added theorem List.length_split_lt

added def List.merge

added def List.mergeSort

added theorem List.mergeSort_cons_cons

added theorem List.mergeSort_eq_insertionSort

added theorem List.mergeSort_eq_self

added theorem List.mergeSort_nil

added theorem List.mergeSort_singleton

added theorem List.monotone_iff_ofFn_sorted

added def List.orderedInsert

added theorem List.orderedInsert_count

added theorem List.orderedInsert_eq_take_drop

added theorem List.orderedInsert_length

added theorem List.orderedInsert_nil

added theorem List.perm_insertionSort

added theorem List.perm_merge

added theorem List.perm_mergeSort

added theorem List.perm_orderedInsert

added theorem List.perm_split

added theorem List.rel_of_sorted_cons

added theorem List.sorted_cons

added theorem List.sorted_insertionSort

added theorem List.sorted_mergeSort

added theorem List.sorted_nil

added theorem List.sorted_singleton

added def List.split

added theorem List.split_cons_of_eq

added theorem List.sublist_of_subperm_of_sorted