mathlib3

0e18561d - doc(metric_space/basic): modify doc for metric spaces adding pseudo metric spaces (#16577)

doc(metric_space/basic): modify doc for metric spaces adding pseudo metric spaces (#16577) The doc preceeding the `pseudo_metric_space` instance spoke only about `metric spaces`. I have added the `pseudo_metric` version.