mathlib3

d292fd7e - refactor(topology/metric_space/basic): add pseudo_metric (#6716)

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.