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} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (s : Set X) : Prop

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.

theorem IsLocallyHomeomorphOn.mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (s : Set X) (h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y) : IsLocallyHomeomorphOn f s

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} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hf : IsLocallyHomeomorphOn f s) {x : X} (hx : x ∈ s) : Filter.map f (nhds x) = nhds (f x)

theorem IsLocallyHomeomorphOn.continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hf : IsLocallyHomeomorphOn f s) {x : X} (hx : x ∈ s) : ContinuousAt f x

theorem IsLocallyHomeomorphOn.continuousOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hf : IsLocallyHomeomorphOn f s) : ContinuousOn f s

theorem IsLocallyHomeomorphOn.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g : Y → Z} {f : X → Y} {s : Set X} {t : Set Y} (hg : IsLocallyHomeomorphOn g t) (hf : IsLocallyHomeomorphOn f s) (h : Set.MapsTo f s t) : IsLocallyHomeomorphOn (g ∘ f) s

def IsLocallyHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop

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.

theorem isLocallyHomeomorph_iff_isLocallyHomeomorphOn_univ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsLocallyHomeomorph f ↔ IsLocallyHomeomorphOn f Set.univ

theorem IsLocallyHomeomorph.isLocallyHomeomorphOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocallyHomeomorph f) : IsLocallyHomeomorphOn f Set.univ

theorem IsLocallyHomeomorph.mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : ∀ (x : X), ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y) : IsLocallyHomeomorph f

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} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocallyHomeomorph f) (x : X) : Filter.map f (nhds x) = nhds (f x)

theorem IsLocallyHomeomorph.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocallyHomeomorph f) : Continuous f

theorem IsLocallyHomeomorph.isOpenMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocallyHomeomorph f) : IsOpenMap f

theorem IsLocallyHomeomorph.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g : Y → Z} {f : X → Y} (hg : IsLocallyHomeomorph g) (hf : IsLocallyHomeomorph f) : IsLocallyHomeomorph (g ∘ f)