mathlib
ac62213b - chore(order/filter/at_top_bot): in `order_top` `at_top = pure ⊤` (#3346)

Commit

5 years ago

chore(order/filter/at_top_bot): in `order_top` `at_top = pure ⊤` (#3346)

Author

urkud

urkud

Parents

Loading