Commit 2025-02-13 11:44 608d54dd

View on Github →

feat(List/Sort): generalize sorted_mergeSort' (#21809) .. to any transitive total relation. Also generalize mergeSort_eq_self to any transitive total antisymmetric relation.

Estimated changes

Modified Mathlib/Data/List/Sort.lean

modified theorem List.mergeSort_eq_insertionSort

modified theorem List.mergeSort_eq_self

modified theorem List.sorted_mergeSort'

Modified Mathlib/Data/Multiset/Sort.lean

Modified Mathlib/Logic/Equiv/List.lean