mathlib
0c1f285a - refactor(topology/metric_space): drop `dist_setoid` (#18502)

Commit

3 years ago

refactor(topology/metric_space): drop `dist_setoid` (#18502) Use `uniform_space.separation_setoid` instead.

Author

urkud

Parents