# Local homeomorphisms #

This file defines local homeomorphisms.

## Main definitions #

For a function f : X → Y  between topological spaces, we say

• IsLocalHomeomorphOn f s if f is a local homeomorphism around each point of s: for each x : X, the restriction of f to some open neighborhood U of x gives a homeomorphism between U and an open subset of Y.
• IsLocalHomeomorph f: f is a local homeomorphism, i.e. it's a local homeomorphism on univ.

Note that IsLocalHomeomorph is a global condition. This is in contrast to PartialHomeomorph, which is a homeomorphism between specific open subsets.

## Main results #

• local homeomorphisms are locally injective open maps
• more!
def IsLocalHomeomorphOn {X : Type u_1} {Y : Type u_2} [] [] (f : XY) (s : Set X) :

A function f : X → Y satisfies IsLocalHomeomorphOn f s if each x ∈ s is contained in the source of some e : PartialHomeomorph X Y with f = e.

Equations
• = xs, ∃ (e : ), x e.source f = e
Instances For
theorem isLocalHomeomorphOn_iff_openEmbedding_restrict {X : Type u_1} {Y : Type u_2} [] [] (s : Set X) {f : XY} :
xs, Unhds x, OpenEmbedding (U.restrict f)
theorem IsLocalHomeomorphOn.mk {X : Type u_1} {Y : Type u_2} [] [] (f : XY) (s : Set X) (h : xs, ∃ (e : ), x e.source Set.EqOn f (e) e.source) :

Proves that f satisfies IsLocalHomeomorphOn f s. The condition h is weaker than the definition of IsLocalHomeomorphOn f s, since it only requires e : PartialHomeomorph X Y to agree with f on its source e.source, as opposed to on the whole space X.

theorem IsLocalHomeomorphOn.PartialHomeomorph.isLocalHomeomorphOn {X : Type u_1} {Y : Type u_2} [] [] (e : ) :
IsLocalHomeomorphOn (e) e.source

A PartialHomeomorph is a local homeomorphism on its source.

theorem IsLocalHomeomorphOn.mono {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} {t : Set X} (hf : ) (hst : s t) :
theorem IsLocalHomeomorphOn.of_comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {g : YZ} {f : XY} {s : Set X} (hgf : IsLocalHomeomorphOn (g f) s) (hg : IsLocalHomeomorphOn g (f '' s)) (cont : xs, ) :
theorem IsLocalHomeomorphOn.of_comp_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {g : YZ} {f : XY} {s : Set X} (hgf : IsLocalHomeomorphOn (g f) s) (hf : ) :
theorem IsLocalHomeomorphOn.map_nhds_eq {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} (hf : ) {x : X} (hx : x s) :
Filter.map f (nhds x) = nhds (f x)
theorem IsLocalHomeomorphOn.continuousAt {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} (hf : ) {x : X} (hx : x s) :
theorem IsLocalHomeomorphOn.continuousOn {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} (hf : ) :
theorem IsLocalHomeomorphOn.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {g : YZ} {f : XY} {s : Set X} {t : Set Y} (hg : ) (hf : ) (h : Set.MapsTo f s t) :
def IsLocalHomeomorph {X : Type u_1} {Y : Type u_2} [] [] (f : XY) :

A function f : X → Y satisfies IsLocalHomeomorph f if each x : x is contained in the source of some e : PartialHomeomorph X Y with f = e.

Equations
• = ∀ (x : X), ∃ (e : ), x e.source f = e
Instances For
theorem Homeomorph.isLocalHomeomorph {X : Type u_1} {Y : Type u_2} [] [] (f : X ≃ₜ Y) :
theorem isLocalHomeomorph_iff_isLocalHomeomorphOn_univ {X : Type u_1} {Y : Type u_2} [] [] {f : XY} :
theorem IsLocalHomeomorph.isLocalHomeomorphOn {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} (hf : ) :
theorem isLocalHomeomorph_iff_openEmbedding_restrict {X : Type u_1} {Y : Type u_2} [] [] {f : XY} :
∀ (x : X), Unhds x, OpenEmbedding (U.restrict f)
theorem OpenEmbedding.isLocalHomeomorph {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
theorem IsLocalHomeomorph.mk {X : Type u_1} {Y : Type u_2} [] [] (f : XY) (h : ∀ (x : X), ∃ (e : ), x e.source Set.EqOn f (e) e.source) :

Proves that f satisfies IsLocalHomeomorph f. The condition h is weaker than the definition of IsLocalHomeomorph f, since it only requires e : PartialHomeomorph X Y to agree with f on its source e.source, as opposed to on the whole space X.

theorem IsLocalHomeomorph.Homeomorph.isLocalHomeomorph {X : Type u_1} {Y : Type u_2} [] [] (h : X ≃ₜ Y) :

A homeomorphism is a local homeomorphism.

theorem IsLocalHomeomorph.isLocallyInjective {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
theorem IsLocalHomeomorph.of_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {g : YZ} {f : XY} (hgf : IsLocalHomeomorph (g f)) (hg : ) (cont : ) :
theorem IsLocalHomeomorph.map_nhds_eq {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) (x : X) :
Filter.map f (nhds x) = nhds (f x)
theorem IsLocalHomeomorph.continuous {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :

A local homeomorphism is continuous.

theorem IsLocalHomeomorph.isOpenMap {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :

A local homeomorphism is an open map.

theorem IsLocalHomeomorph.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {g : YZ} {f : XY} (hg : ) (hf : ) :

The composition of local homeomorphisms is a local homeomorphism.

theorem IsLocalHomeomorph.openEmbedding_of_injective {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) (hi : ) :

An injective local homeomorphism is an open embedding.

noncomputable def Embedding.toHomeomeomorph_of_surjective {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) (hsurj : ) :
X ≃ₜ Y

A surjective embedding is a homeomorphism.

Equations
• hf.toHomeomeomorph_of_surjective hsurj =
Instances For
noncomputable def IsLocalHomeomorph.toHomeomorph_of_bijective {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) (hb : ) :
X ≃ₜ Y

A bijective local homeomorphism is a homeomorphism.

Equations
• hf.toHomeomorph_of_bijective hb =
Instances For
theorem IsLocalHomeomorph.openEmbedding_of_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {g : YZ} {f : XY} (hf : ) (hgf : OpenEmbedding (g f)) (cont : ) :

Continuous local sections of a local homeomorphism are open embeddings.

theorem IsLocalHomeomorph.isTopologicalBasis {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
TopologicalSpace.IsTopologicalBasis {U : Set X | ∃ (V : Set Y), ∃ (s : C(V, X)), f s = Subtype.val = U}

Ranges of continuous local sections of a local homeomorphism form a basis of the source space.