mathlib

ddb46177 - refactor(topology/metric_space/isometry): move Kuratowski embedding to another file (#6678)

refactor(topology/metric_space/isometry): move Kuratowski embedding to another file (#6678) This reduces the import dependencies of `topology.metric_space.isometry`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>