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 <25c750517795e47f172dc8c552ed72c7de260bd4@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib