mathlib

5ecd078d - feat(data/ordmap/ordset): Implement some more `ordset` functions (#8127)

feat(data/ordmap/ordset): Implement some more `ordset` functions (#8127) Implement (with proofs) `erase`, `map`, and `mem` for `ordset` in `src/data/ordmap` along with a few useful related proofs.