Local homeomorphisms #
This file defines local homeomorphisms.
Main definitions #
-
is_locally_homeomorph
: A functionf : X → Y
satisfiesis_locally_homeomorph
if for each pointx : X
, the restriction off
to some open neighborhoodU
ofx
gives a homeomorphism betweenU
and an open subset ofY
.Note that
is_locally_homeomorph
is a global condition. This is in contrast tolocal_homeomorph
, which is a homeomorphism between specific open subsets.
A function f : X → Y
satisfies is_locally_homeomorph
if each x : x
is contained in
the source of some e : local_homeomorph X Y
with f = e
.
Equations
- is_locally_homeomorph f = ∀ (x : X), ∃ (e : local_homeomorph X Y), x ∈ e.to_local_equiv.source ∧ f = ⇑e
Proves that f
satisfies is_locally_homeomorph
. The condition h
is weaker than definition
of is_locally_homeomorph
, since it only requires e : local_homeomorph X Y
to agree with f
on
its source e.source
, as opposed to on the whole space X
.