Commit 2026-08-03 21:26 9fb10993

View on Github →

feat(Topology/Order): the bornology of an unbounded order is non-trivial (#42030) Also generalise the fact that cobounded sets tend to top/bot from linear orders to preorders (without a max/min element).

Estimated changes