Theorem Nonempty.of_isOrderBornology

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) …
Added Nonempty.of_isOrderBornologyView on Github →