Metric quotients of pseudometric spaces

[malarbol]

This PR introduces the notion of metric quotient of a pseudometric spaces: the metric space whose objects are quotient classes under the similarity relation in the pseudometric spaces and rational neighborhood relations given by neighborhoods of class-elements.

This is a metric space isometric to the original pseudometric space. In case of metric spaces, this isometry is an isometric equivalence. Any short map (resp. isometry) from a pseudometric space to a metric space factors as a short map (resp. isometry) through the metric quotient.

The module cauchy-approximations-metric-quotients-of-pseudometric-spaces introduces a few results regarding Cauchy approximations in pseudometric spaces and Cauchy approximations in their metric quotients.

Co-authored-by: Louis Wasserman wasserman.louis@gmail.com

[malarbol]

This is part (3/4) of my work towards #1458.

The last part is basically to take the metric quotient of the Cauchy pseudocompletion and work with that. It behaves like a Cauchy completion in a lot of ways but, as discussed in #1458, we can't prove that it is Cauchy complete.

[fredrik-bakke]

I wonder if "metric space quotient" is a better name for this concept. The term "metric quotient" seems a little vague, like, one could for instance mistakenly interpret it as quotienting by the metric, or some metric.

[malarbol]

so, Is "metric quotient" ok for now (c.f. #1622) or do you want be to change the headers to refer to "metric space quotients" and/or the name of the construction metric-space-quotient-Pseudometric-Space?
(I still find the first space too much, but as you wish).

[fredrik-bakke]

"Metric quotient" is, I think, too vague. It doesn't describe what you are constructing, it seems to me that it is a short hand.

[malarbol]

one could for instance mistakenly interpret it as quotienting by the metric, or some metric.

I'm not sure about this:

1. nowhere do we use metric as a noun (we use distance for that) so there's nothing in the library that could create such confusion;
2. you can only quotient by an equivalence relation so "quotienting by a metric" doesn't really make sense.

"Metric quotient" is, I think, too vague. It doesn't describe what you are constructing, it seems to me that it is a short hand.

I think it does. There's a more general construction of quotient-Pseudometric-Space considering quotients of Pseudometric spaces by an equivalence relation compatible with the pseudometric structure and this is a bottom case where the quotient-Pseudometric-Space you construct is metric (used as an adjective), hence metric-quotient-Pseudometric-Space.

I still find metric-space-quotient-Pseudometric-Space too redundant. space is the less relevant noun of the name and is there twice.

Could we have external opinions from @lowasser or @VojtechStep maybe?