Theorem DiscreteTopology.of_predOrder_succOrder

Modification history

2024-11-11 05:16

Mathlib/Topology/Order/OrderClosed.lean

feat(Topology/Order): add more `CovBy.nhdsWithin...` lemmas (#18567) …

Added DiscreteTopology.of_predOrder_succOrder View on Github →