Commit 2023-05-22 05:47 94a92f15

View on Github →

feat: port Topology.MetricSpace.Metrizable (#4181)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Metrizable.lean

added theorem Embedding.metrizableSpace

added theorem Inducing.pseudoMetrizableSpace

added theorem TopologicalSpace.exists_embedding_l_infty

added theorem TopologicalSpace.metrizableSpace_of_t3_second_countable