Theorem disjoint_nhds_atTop_iff

Modification history

2024-02-22 12:56
Mathlib/Topology/Order/OrderClosed.lean
feat(Topology/Order): generalize disjoint_nhds_atTop (#10580) …
Added disjoint_nhds_atTop_iffView on Github →