Local homeomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_on {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] (f : X → Y) (s : set X) :

Prop

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

Equations

is_locally_homeomorph_on f s = ∀ (x : X), x ∈ s → (∃ (e : local_homeomorph X Y), x ∈ e.to_local_equiv.source ∧ f = ⇑e)

source

theorem is_locally_homeomorph_on.mk {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] (f : X → Y) (s : set X) (h : ∀ (x : X), x ∈ s → (∃ (e : local_homeomorph X Y), x ∈ e.to_local_equiv.source ∧ ∀ (y : X), y ∈ e.to_local_equiv.source → f y = ⇑e y)) :

is_locally_homeomorph_on f s

Proves that f satisfies is_locally_homeomorph_on f s. The condition h is weaker than the definition of is_locally_homeomorph_on f s, 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.

source

theorem is_locally_homeomorph_on.map_nhds_eq {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} {s : set X} (hf : is_locally_homeomorph_on f s) {x : X} (hx : x ∈ s) :

filter.map f (nhds x) = nhds (f x)

source

@[protected]

theorem is_locally_homeomorph_on.continuous_at {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} {s : set X} (hf : is_locally_homeomorph_on f s) {x : X} (hx : x ∈ s) :

continuous_at f x

source

@[protected]

theorem is_locally_homeomorph_on.continuous_on {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} {s : set X} (hf : is_locally_homeomorph_on f s) :

continuous_on f s

source

@[protected]

theorem is_locally_homeomorph_on.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [topological_space X] [topological_space Y] [topological_space Z] {g : Y → Z} {f : X → Y} {s : set X} {t : set Y} (hg : is_locally_homeomorph_on g t) (hf : is_locally_homeomorph_on f s) (h : set.maps_to f s t) :

is_locally_homeomorph_on (g ∘ f) s

source

def is_locally_homeomorph {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] (f : X → Y) :

Prop

A function f : X → Y satisfies is_locally_homeomorph f 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

source

theorem is_locally_homeomorph_iff_is_locally_homeomorph_on_univ {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} :

is_locally_homeomorph f ↔ is_locally_homeomorph_on f set.univ

source

@[protected]

theorem is_locally_homeomorph.is_locally_homeomorph_on {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} (hf : is_locally_homeomorph f) :

is_locally_homeomorph_on f set.univ

source

theorem is_locally_homeomorph.mk {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] (f : X → Y) (h : ∀ (x : X), ∃ (e : local_homeomorph X Y), x ∈ e.to_local_equiv.source ∧ ∀ (y : X), y ∈ e.to_local_equiv.source → f y = ⇑e y) :

is_locally_homeomorph f

Proves that f satisfies is_locally_homeomorph f. The condition h is weaker than the definition of is_locally_homeomorph f, 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.

source

theorem is_locally_homeomorph.map_nhds_eq {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} (hf : is_locally_homeomorph f) (x : X) :

filter.map f (nhds x) = nhds (f x)

source

@[protected]

theorem is_locally_homeomorph.continuous {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} (hf : is_locally_homeomorph f) :

continuous f

source

@[protected]

theorem is_locally_homeomorph.is_open_map {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} (hf : is_locally_homeomorph f) :

is_open_map f

source

@[protected]

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

is_locally_homeomorph (g ∘ f)