Commit 2021-03-17 03:47 d292fd7e
View on Github →refactor(topology/metric_space/basic): add pseudo_metric (#6716)
This is the natural continuation of #6694: we introduce here pseudo_metric_space
.
Note that I didn't do anything fancy, I only generalize the results that work out of the box for pseudometric spaces (quite a lot indeed).
It's possible that there is some duplicate code, especially in the section about products.