Documentation

Mathlib.Topology.IsLocalHomeomorph

Local homeomorphisms #

This file defines local homeomorphisms.

Main definitions #

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

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

Main results #

def IsLocalHomeomorphOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (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
Instances For
    theorem isLocalHomeomorphOn_iff_openEmbedding_restrict {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) {f : XY} :
    IsLocalHomeomorphOn f s xs, Unhds x, OpenEmbedding (U.restrict f)
    theorem IsLocalHomeomorphOn.mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (s : Set X) (h : xs, ∃ (e : PartialHomeomorph X Y), 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.

    A PartialHomeomorph is a local homeomorphism on its source.

    theorem IsLocalHomeomorphOn.mono {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set X} {t : Set X} (hf : IsLocalHomeomorphOn f t) (hst : s t) :
    theorem IsLocalHomeomorphOn.of_comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g : YZ} {f : XY} {s : Set X} (hgf : IsLocalHomeomorphOn (g f) s) (hg : IsLocalHomeomorphOn g (f '' s)) (cont : xs, ContinuousAt f x) :
    theorem IsLocalHomeomorphOn.of_comp_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g : YZ} {f : XY} {s : Set X} (hgf : IsLocalHomeomorphOn (g f) s) (hf : IsLocalHomeomorphOn f s) :
    theorem IsLocalHomeomorphOn.map_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set X} (hf : IsLocalHomeomorphOn f s) {x : X} (hx : x s) :
    Filter.map f (nhds x) = nhds (f x)
    theorem IsLocalHomeomorphOn.continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set X} (hf : IsLocalHomeomorphOn f s) {x : X} (hx : x s) :
    theorem IsLocalHomeomorphOn.continuousOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set X} (hf : IsLocalHomeomorphOn f s) :
    theorem IsLocalHomeomorphOn.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g : YZ} {f : XY} {s : Set X} {t : Set Y} (hg : IsLocalHomeomorphOn g t) (hf : IsLocalHomeomorphOn f s) (h : Set.MapsTo f s t) :
    def IsLocalHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (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
    Instances For
      theorem isLocalHomeomorph_iff_openEmbedding_restrict {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} :
      IsLocalHomeomorph f ∀ (x : X), Unhds x, OpenEmbedding (U.restrict f)
      theorem IsLocalHomeomorph.mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (h : ∀ (x : X), ∃ (e : PartialHomeomorph X Y), 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.

      A homeomorphism is a local homeomorphism.

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

      A local homeomorphism is continuous.

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

      A local homeomorphism is an open map.

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

      The composition of local homeomorphisms is a local homeomorphism.

      An injective local homeomorphism is an open embedding.

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

      A surjective embedding is a homeomorphism.

      Equations
      Instances For
        noncomputable def IsLocalHomeomorph.toHomeomorph_of_bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsLocalHomeomorph f) (hb : Function.Bijective f) :
        X ≃ₜ Y

        A bijective local homeomorphism is a homeomorphism.

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

          Continuous local sections of a local homeomorphism are open embeddings.

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

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