distance preserving maps

Stream: Is there code for X?

[Johan Commelin]

Do we have isometries?

[Johan Commelin]

I've never really used metric spaces in mathlib... don't know the library

[Chris Hughes]

topology/metric_space/isometry.lean looks good.

[Johan Commelin]

Weird... I don't know how I missed that.

[Johan Commelin]

I did a code search for isome*

[Johan Commelin]

@Sebastien Gouezel Is there a reason that you included this line https://github.com/leanprover-community/mathlib/blob/93ba8b6d19fc4b93c862de99e0021b502c7e9126/src/topology/metric_space/isometry.lean#L113?

[Johan Commelin]

Because a few lines above it, you proved that it follows from L112

[Sebastien Gouezel]

I don't remember. Indeed it could be removed at no cost, but having it there makes for a more symmetrical definition, and you have direct access to the fields i.isometry_to_fun and i.isometry_inv_fun. Otherwise, it would be a lemma, and basically it wouldn't make any difference. So, no strong opinion in one direction or the other.

[Johan Commelin]

If we leave it like this, I guess it would make sense to have a constructor that doesn't require it. Because right now we're shifting the proof-obligation to the user, which is maybe not what we want.

[Sebastien Gouezel]

Absolutely. The best move is probably to remove the line from the definition, and add a lemma isometric.isometry_inv_fun.

[Johan Commelin]

#2051

[Sebastien Gouezel]

Thanks!