Mathlib v3 is deprecated. Go to Mathlib v4

Theorem embedding.discrete_topology

Modification history

2023-01-30 21:46
src/topology/maps.lean
refactor(topology/{order,*}): review API (#18312) …
Modified embedding.discrete_topologyView on Github →
2022-09-02 10:49
src/topology/separation.lean
feat(topology/separation): `embedding.discrete_topology` (#16092) …
Added embedding.discrete_topologyView on Github →