# mathlibdocumentation

topology.is_locally_homeomorph

# Local homeomorphisms #

This file defines local homeomorphisms.

## Main definitions #

• is_locally_homeomorph: A function f : X → Y satisfies is_locally_homeomorph 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 is_locally_homeomorph is a global condition. This is in contrast to local_homeomorph, which is a homeomorphism between specific open subsets.

def is_locally_homeomorph {X : Type u_1} {Y : Type u_2} (f : X → Y) :
Prop

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
• = ∀ (x : X), ∃ (e : Y), f = e
theorem is_locally_homeomorph.mk {X : Type u_1} {Y : Type u_2} (f : X → Y) (h : ∀ (x : X), ∃ (e : Y), ∀ (x : X), f x = e x) :

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.

theorem is_locally_homeomorph.map_nhds_eq {X : Type u_1} {Y : Type u_2} {f : X → Y} (hf : is_locally_homeomorph f) (x : X) :
(nhds x) = nhds (f x)
@[protected]
theorem is_locally_homeomorph.continuous {X : Type u_1} {Y : Type u_2} {f : X → Y} (hf : is_locally_homeomorph f) :
theorem is_locally_homeomorph.is_open_map {X : Type u_1} {Y : Type u_2} {f : X → Y} (hf : is_locally_homeomorph f) :
@[protected]
theorem is_locally_homeomorph.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {g : Y → Z} {f : X → Y} (hg : is_locally_homeomorph g) (hf : is_locally_homeomorph f) :