Commit 2025-03-03 08:08 07c9b41a

View on Github →

feat(List/Sort): add lemmas about (l.map f).Sorted _ (#22426)

Estimated changes

Modified Mathlib/Data/List/Sort.lean

added theorem OrderEmbedding.sorted_gt_listMap

added theorem OrderEmbedding.sorted_lt_listMap

added theorem OrderIso.sorted_gt_listMap

added theorem OrderIso.sorted_lt_listMap

added theorem RelEmbedding.sorted_listMap

added theorem RelEmbedding.sorted_swap_listMap

added theorem RelIso.sorted_listMap

added theorem RelIso.sorted_swap_listMap

added theorem StrictAnti.sorted_ge_listMap

added theorem StrictAnti.sorted_gt_listMap

added theorem StrictAnti.sorted_le_listMap

added theorem StrictAnti.sorted_lt_listMap

added theorem StrictMono.sorted_ge_listMap

added theorem StrictMono.sorted_gt_listMap

added theorem StrictMono.sorted_le_listMap

added theorem StrictMono.sorted_lt_listMap