Documentation

Mathlib.Topology.IsLocallyHomeomorph

Local homeomorphisms #

This file defines local homeomorphisms.

Main definitions #

• IsLocallyHomeomorph: A function f : X → Y satisfies IsLocallyHomeomorph if for each point x : X, the restriction of f to some open neighborhood U of x gives a homeomorphism between U and an open subset of Y.

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

def IsLocallyHomeomorphOn {X : Type u_1} {Y : Type u_2} [] [] (f : XY) (s : Set X) :

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

Instances For
theorem IsLocallyHomeomorphOn.mk {X : Type u_1} {Y : Type u_2} [] [] (f : XY) (s : Set X) (h : ∀ (x : X), x se, x e.source ∀ (y : X), y e.sourcef y = e y) :

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

theorem IsLocallyHomeomorphOn.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 IsLocallyHomeomorphOn.continuousAt {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} (hf : ) {x : X} (hx : x s) :
theorem IsLocallyHomeomorphOn.continuousOn {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} (hf : ) :
theorem IsLocallyHomeomorphOn.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 IsLocallyHomeomorph {X : Type u_1} {Y : Type u_2} [] [] (f : XY) :

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

Instances For
theorem isLocallyHomeomorph_iff_isLocallyHomeomorphOn_univ {X : Type u_1} {Y : Type u_2} [] [] {f : XY} :
theorem IsLocallyHomeomorph.isLocallyHomeomorphOn {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
theorem IsLocallyHomeomorph.mk {X : Type u_1} {Y : Type u_2} [] [] (f : XY) (h : ∀ (x : X), e, x e.source ∀ (y : X), y e.sourcef y = e y) :

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

theorem IsLocallyHomeomorph.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 IsLocallyHomeomorph.continuous {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
theorem IsLocallyHomeomorph.isOpenMap {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
theorem IsLocallyHomeomorph.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {g : YZ} {f : XY} (hg : ) (hf : ) :