mathlib

3c927487 - feat(topology/separation): `embedding.discrete_topology` (#16092)

feat(topology/separation): `embedding.discrete_topology` (#16092) This PR adds a short lemma `embedding.discrete_topology` and golfs the related lemma `discrete_topology_induced`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>