Theorem IsOrderBornology.cobounded_le_atBot_sup_atTop

Modification history

2026-08-03 21:26
Mathlib/Topology/Order/Bornology.lean
feat(Topology/Order): the bornology of an unbounded order is non-trivial (#42030) …
Modified IsOrderBornology.cobounded_le_atBot_sup_atTopView on Github →
2026-04-28 16:44
Mathlib/Topology/Order/Bornology.lean
feat(Topology/Order/Bornology): generalize `cobounded_eq` (#37738) …
Added IsOrderBornology.cobounded_le_atBot_sup_atTopView on Github →