Mathlib v3 is deprecated. Go to Mathlib v4

Def emetric_space.to_metric_space

Modification history

2023-03-01 18:06
src/topology/metric_space/basic.lean
refactor(topology/uniform_space/basic): review API (#18516) …
Modified emetric_space.to_metric_spaceView on Github →
2019-01-28 19:34
src/topology/metric_space/basic.lean
add ennreal.to_real
Added emetric_space.to_metric_spaceView on Github →