mathlib3
39a3b58b - feat(order/filter/at_top_bot): `order_iso` maps `at_top` to `at_top` (#5236)

Commit

5 years ago

feat(order/filter/at_top_bot): `order_iso` maps `at_top` to `at_top` (#5236)

Author

urkud

urkud

Parents

Loading