Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-03-25 18:48
221796ab
View on Github →
feat(topology/metric_space/metrizable): define and use a metrizable typeclass (
#12934
)
Estimated changes
Modified
src/topology/instances/ennreal.lean
Modified
src/topology/metric_space/metrizable.lean
added
theorem
embedding.metrizable_space
added
theorem
topological_space.metrizable_space_of_normal_second_countable