Commit 2021-03-15 22:29 ddb46177

View on Github →

refactor(topology/metric_space/isometry): move Kuratowski embedding to another file (#6678) This reduces the import dependencies of topology.metric_space.isometry.

Estimated changes

Modified src/topology/metric_space/closeds.lean

Modified src/topology/metric_space/gromov_hausdorff.lean

Modified src/topology/metric_space/gromov_hausdorff_realized.lean

Modified src/topology/metric_space/isometry.lean

deleted def Kuratowski_embedding.embedding_of_subset

deleted theorem Kuratowski_embedding.embedding_of_subset_coe

deleted theorem Kuratowski_embedding.embedding_of_subset_dist_le

deleted theorem Kuratowski_embedding.embedding_of_subset_isometry

deleted theorem Kuratowski_embedding.exists_isometric_embedding

deleted def Kuratowski_embedding

deleted def nonempty_compacts.Kuratowski_embedding

deleted def ℓ_infty_ℝ

Created src/topology/metric_space/kuratowski.lean

added def Kuratowski_embedding.embedding_of_subset

added theorem Kuratowski_embedding.embedding_of_subset_coe

added theorem Kuratowski_embedding.embedding_of_subset_dist_le

added theorem Kuratowski_embedding.embedding_of_subset_isometry

added theorem Kuratowski_embedding.exists_isometric_embedding

added def Kuratowski_embedding

added def nonempty_compacts.Kuratowski_embedding

added def ℓ_infty_ℝ