Commit 2023-06-01 10:18 a8e87892

View on Github →

feat: port Topology.MetricSpace.Kuratowski (#4544)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Kuratowski.lean

added def KuratowskiEmbedding.embeddingOfSubset

added theorem KuratowskiEmbedding.embeddingOfSubset_coe

added theorem KuratowskiEmbedding.embeddingOfSubset_dist_le

added theorem KuratowskiEmbedding.embeddingOfSubset_isometry

added theorem KuratowskiEmbedding.exists_isometric_embedding

added def kuratowskiEmbedding