Theorem KuratowskiEmbedding.embeddingOfSubset_dist_le

Modification history

2023-06-01 10:18
Mathlib/Topology/MetricSpace/Kuratowski.lean
feat: port Topology.MetricSpace.Kuratowski (#4544)
Added KuratowskiEmbedding.embeddingOfSubset_dist_leView on Github →