Isometries

[sgouezel]

Add isometries between emetric or metric spaces, and prove their basic properties.

[johoelzl]

I would propose two changes:

1. the set is not necessary, metric spaces behave nice under subtype restriction.
2. As far as I understand, isometries are metric equivalences? Would it make sense to extend equiv with a metric restriction, and then provide a function mapping it into a homeomorphism? Also providing a constructor for just one direction and a proof of surjectivity.

[johoelzl]

Also, couldn't one proof that a emtric.isometry is the same as the metric.isometry on metric spaces? Then no additional constant is needed

[sgouezel]

1 - Yes, I will remove the set
2 - The notion in this PR is isometric embedding, not isometric isomorphism (i.e., isometries don't have to be onto). It definitely makes sense to introduce a notion of isometric isomorphism (i.e., an equiv in which both maps are isometries, or equivalently one of them is an isometry and then the other one is automatically), but it can maybe wait for a futher PR.
3 - Yes, the two notions are equivalent on a metric space. This is proved in emetric_isometry_on_iff_isometry_on. I agree it will be better to have just one constant isometry, probably in the root namespace (or is there a way to put it in emetric, but to export it automatically in metric?)

[johoelzl]

Ah, I didn't realize that it is a embedding. And of course, isometric isomorphisms are for another PR.

I'm fine with putting isometry in the root namespace.

[jcommelin]

[...] I agree it will be better to have just one constant isometry, probably in the root namespace (or is there a way to put it in emetric, but to export it automatically in metric?)

I think, if you want this to happen automatically then metric would have to extend emetric, but this is not the current setup.

[rwbarton]

You can write something like (in the metric namespace) export emetric (isometry) although I'm not sure exactly what it does.

[sgouezel]

I have removed the set, and unified the emetric and metric notions. I have also added a section on isometric isomorphisms, since they will be needed anyway. I wasn't sure between bundled and unbundled approaches, so in the end I adapted what is done for homeomorphisms but I am open to suggestions.