Theorem discreteTopology_iff_orderTopology_of_pred_succ

Modification history

2023-05-30 04:33
Mathlib/Topology/Instances/Discrete.lean
feat: port Topology.Instances.Discrete (#4479)
Added discreteTopology_iff_orderTopology_of_pred_succView on Github →