Zulip Chat Archive

Stream: Is there code for X?

Topic: distance preserving maps


view this post on Zulip Johan Commelin (Feb 24 2020 at 07:00):

Do we have isometries?

view this post on Zulip Johan Commelin (Feb 24 2020 at 07:01):

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

view this post on Zulip Chris Hughes (Feb 24 2020 at 07:25):

topology/metric_space/isometry.lean looks good.

view this post on Zulip Johan Commelin (Feb 24 2020 at 07:35):

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

view this post on Zulip Johan Commelin (Feb 24 2020 at 07:35):

I did a code search for isome*

view this post on Zulip Johan Commelin (Feb 24 2020 at 16:23):

@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?

view this post on Zulip Johan Commelin (Feb 24 2020 at 16:24):

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

view this post on Zulip Sebastien Gouezel (Feb 24 2020 at 16:30):

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.

view this post on Zulip Johan Commelin (Feb 24 2020 at 17:20):

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.

view this post on Zulip Sebastien Gouezel (Feb 24 2020 at 17:57):

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

view this post on Zulip Johan Commelin (Feb 24 2020 at 19:14):

#2051

view this post on Zulip Sebastien Gouezel (Feb 24 2020 at 19:48):

Thanks!


Last updated: May 17 2021 at 15:13 UTC