Commit 2022-09-02 10:49 3c927487

View on Github →

feat(topology/separation): embedding.discrete_topology (#16092) This PR adds a short lemma embedding.discrete_topology and golfs the related lemma discrete_topology_induced.

Estimated changes

Modified src/topology/separation.lean

added theorem embedding.discrete_topology