Theorem notBelow_isOpen

Modification history

2025-07-02 15:47

Mathlib/Topology/OmegaCompletePartialOrder.lean

chore: deprecate `Scott` in favour of `WithScott` (#26619) …

Modified notBelow_isOpen View on Github →

2023-02-03 07:53

Mathlib/Topology/OmegaCompletePartialOrder.lean

feat: port Topology.OmegaCompletePartialOrder (#2034)

Added notBelow_isOpen View on Github →