Naming around local homeomorphisms

Stream: mathlib4

[Michael Rothgang]

Right now, mathlib has LocalHomeomorph and IsLocallyHomeomorph: these sound very similar, but are in fact different.
The latter is called a "local homeomorphism" in informal, textbook mathematics. The former could rather be called a partial homeomorphism: it's a homeomorphism on an open set of the domain (extended to the whole space, by the junk value pattern). I would prefer renaming these.

• @Floris van Doorn suggested renaming LocalHomeomorph to PartialHomeomorph (I have a wip branch performing this rename)
• I would prefer renaming IsLocallyHomeomorph to IsLocalHomeomorph. I don't see a good reason to deviate from math terminology. (This would match IsLocalStructomorphWithinAt. It is different from IsLocallyInjective; I'd argue this is different since one would always speak of a "locally injective map".)
  @Thomas Browning You wrote this file; do you see a reason not to do this?

[Yury G. Kudryashov]

AFAIR, the main reason for naming docs#IsLocallyHomeomorph was to avoid renaming of LocalHomeomorph mid-port.

[Yury G. Kudryashov]

And the main issue with PartialHomeomorph (and, I guess, PartialEquiv) is that it's too similar to docs#PEquiv (AFAICT, mostly unused in Mathlib).

[Thomas Browning]

Yes, I agree that the naming is confusing right now. If a better pair of names is found, I don't see any reason not to rename. But it would be good to keep the names of LocalEquiv and LocalHomeomorph similar to each other.

[Floris van Doorn]

I'm in favor of renaming LocalEquiv to PartialEquiv and LocalHomeomorph to PartialHomeomorph. I think it's fine to have similar names PEquiv and PartialEquiv, since they also mean almost the same thing.

[Michael Rothgang]

Sounds like there is consensus (among those speaking up) for the new names, great.
I've submitted #8982 for renaming LocalHomeomorph; LocalEquiv is up for volunteers (or I'll do it later this week).

[Michael Rothgang]

And #8983 for IsLocallyHomeomorph{On}.

[Michael Rothgang]

Actually, I've just done LocalEquiv also: #8984
Doesn't lint (line length); feel free to jump in and fix these (or I'll do it later).