Stream: general

Topic: left/right for source/target

Yury G. Kudryashov (Mar 05 2021 at 17:06):

Some lemmas about docs#local_equiv and docs#local_homeomorph deal with e.source ∩ s / e.target ∩ t, some with s ∩ e.source/s ∩ e.target. I'm trying to define local_homeomorph.piecewise and quite often I have to rw inter_comm to apply the lemma I want. Some lemma, e.g., docs#local_equiv.image_inter_source_eq, mix "left" and "right" conventions.
@Sebastien Gouezel You're the author of local_equiv. Is there some convention I miss? If no, what do you think about normalizing the lemmas to always put e.source/e.target on one side of ∩?

Yury G. Kudryashov (Mar 05 2021 at 17:07):

See #6555 for local_equiv.piecewise.

Yury G. Kudryashov (Mar 05 2021 at 17:14):

Another question: there are many ways to say that t : set β is the image of s : set α under e : local_equiv α β when restricted to e.source/e.target.
This relation is closed under normal set operations and in the case of a local_homeomorph it is also closed under closure/frontier/interior. What do you think about giving it a name?

Sebastien Gouezel (Mar 05 2021 at 17:37):

Sure, it is a good idea to try to normalize. I have tried to be coherent when writing these files, but I have probably missed some places. Also, when you use lemmas from other parts of mathlib, conventions are not always the same, so it ended a little bit random. Choosing one side once and for all would definitely be an improvement!

Sebastien Gouezel (Mar 05 2021 at 17:37):

Yury G. Kudryashov said:

Another question: there are many ways to say that t : set β is the image of s : set α under e : local_equiv α β when restricted to e.source/e.target.
This relation is closed under normal set operations and in the case of a local_homeomorph it is also closed under closure/frontier/interior. What do you think about giving it a name?

Yes, that's a good idea!

Yury G. Kudryashov (Mar 05 2021 at 17:39):

How would you name it?

Sebastien Gouezel (Mar 05 2021 at 17:48):

t = local_equiv.image e s? I know it does not really correspond to set.image, but still it sounds ok to me.

Yury G. Kudryashov (Mar 05 2021 at 18:27):

This is not an equality t = f s, it's t ∩ e.target = e '' (s ∩ e.source). local_equiv.is_image e s t?

Sebastien Gouezel (Mar 05 2021 at 19:27):

I thought you wanted t to already be a subset of e.target, but I agree your version is better as it is more symmetric. Yes, e.is_image s t looks good.

Eric Wieser (Mar 05 2021 at 19:33):

Is this at all similar to docs#set.bij_on?

Eric Wieser (Mar 05 2021 at 19:34):

Suggesting perhaps e.bij_on for consistency