Metric extensions

[malarbol]

Built on top of #1738

This PR introduces the following concepts:

• extension-Pseudometric-Space P: a pseudometric space Q with an isometry i : P → Q;
• extension-Metric-Space M: a metric space N with an isometry i : M → N;
• Metric-Extension P : a metric space M with an isometry i : P → M. This is equivalent to extensional extensions of pseudometric spaces.

[fredrik-bakke]

What you call a Metric-Extension should really be called something of the form is-metric-extension. A metric extension of P would be a choice of a metric space M together with an isometry. I.e., the M is bundled with the isometry. I am still entirely unconvinced about the terminology choice of Metric-Extension, though, but I haven't come up with a better name which is why you haven't heard from me.

[fredrik-bakke]

I believe* it should be called is-extension-metric-space-Pseudometric-Space, and presumably you would want the rest of your formalizations to be in terms of the bundled version instead, whatever that should be called. Potentially extension-metric-space-Pseudometric-Space.

[fredrik-bakke]

another candidate is extensional-extension-Pseudometric-Space, although I like that less

[fredrik-bakke]

it would fit into a larger picture though, together with extensional extensions of preorders and strictly* preordered sets, and such things.