Theorem DiscreteTopology.of_continuous_injective

Modification history

2023-09-08 13:40
Mathlib/Topology/Order.lean
feat: add `DiscreteTopology.of_continuous_injective` (#7029)
Added DiscreteTopology.of_continuous_injectiveView on Github →