Zulip Chat Archive

Stream: Is there code for X?

Topic: Local homeomorphisms

Thomas Browning (Dec 09 2021 at 20:38):

Does mathlib have a definition of https://en.wikipedia.org/wiki/Local_homeomorphism?

topology/local_homeomorph.lean has a slightly different notion, involving a homeomorphism between two open subsets.

Yury G. Kudryashov (Dec 09 2021 at 21:55):

I don't think that we have this definition. @Sebastien Gouezel @Patrick Massot @Heather Macbeth What name would you prefer to distinguish these two notions in mathlib?

Yury G. Kudryashov (Dec 09 2021 at 21:56):

is_local_homeomorph?

Yury G. Kudryashov (Dec 09 2021 at 21:57):

Is it equivalent to ∀ x : X, ∃ e : local_homeomorph X Y, (e : X → Y) = f ∧ x ∈ e.source?

Sebastien Gouezel (Dec 10 2021 at 07:37):

locally_homeomorph?

Last updated: Dec 20 2023 at 11:08 UTC