Theorem discreteTopology_iff_orderTopology_of_pred_succ'
Modification history
2024-11-11 05:16
Mathlib/Topology/Instances/Discrete.lean
feat(Topology/Order): add more `CovBy.nhdsWithin...` lemmas (#18567) …
Deleted discreteTopology_iff_orderTopology_of_pred_succ'View on Github →