left/right for source/target

Stream: general

[Yury G. Kudryashov]

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]

See #6555 for local_equiv.piecewise.

[Yury G. Kudryashov]

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]

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]

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]

How would you name it?

[Sebastien Gouezel]

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]

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]

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]

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

[Eric Wieser]

Suggesting perhaps e.bij_on for consistency

[Yury G. Kudryashov]

docs#local_equiv.bij_on already exists