Def kuratowskiEmbedding

Modification history

2023-06-18 00:43
Mathlib/Topology/MetricSpace/Kuratowski.lean
feat: Lipschitz extensions of maps into l^infty (#5107) …
Modified kuratowskiEmbeddingView on Github →
2023-06-01 10:18
Mathlib/Topology/MetricSpace/Kuratowski.lean
feat: port Topology.MetricSpace.Kuratowski (#4544)
Added kuratowskiEmbeddingView on Github →