Lemmas metric spaces

[malarbol]

This PR introduces a few lemmas on (pseudo)metric spaces.

• any complete metric space is a retract of its metric space of Cauchy approximations;
• constant Cauchy approximations are convergent;
• any metric space is a retract of its convergent Cauchy approximations;
• short maps from a pseudometric space to a metric space reflect similarity.

[fredrik-bakke]

Nice work, and it's nice to see you're active again :)

[malarbol]

it's nice to see you're active again :)

thanks. I needed a little break after this summer.
This is the first split of #1507 (as discussed in #1458 (comment)). I hoped to get further down the notion of Cauchy completion but this is the best I could do.

There will be upcoming PRs for

• pseudometric completions of (pseudo)metric spaces;
• metric quotients of pseudometric spaces;
• metric pseudocompletion of (pseudo)metric spaces (the metric quotient of the pseudometric completion).

[fredrik-bakke]

Looking forward to it!