Commit 2024-03-07 21:56 0c4cb825

View on Github →

feat: results about List.orderedInsert (#11191) I suspect I will need some of these for #10660

Estimated changes

Modified Mathlib/Data/List/Sort.lean

added theorem List.erase_orderedInsert

added theorem List.erase_orderedInsert_of_not_mem

added theorem List.mem_orderedInsert

added theorem List.orderedInsert_erase

added theorem List.sublist_orderedInsert

Modified Mathlib/Init/Algebra/Classes.lean