Commit 2023-09-08 13:40 bb3c2eb4

View on Github →

feat: add DiscreteTopology.of_continuous_injective (#7029)

Estimated changes

Modified Mathlib/Topology/Maps.lean

modified theorem Embedding.discreteTopology

Modified Mathlib/Topology/Order.lean

added theorem DiscreteTopology.of_continuous_injective