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_isOpenEmbedding_restrict {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) {f : XY} :
      IsLocalHomeomorphOn f s xs, Unhds x, Topology.IsOpenEmbedding (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.

      theorem IsLocalHomeomorphOn.mono {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s 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

          A space that admits a local homeomorphism to a discrete space is itself discrete.

          If there is a surjective local homeomorphism between two spaces and one of them is discrete, then both spaces are discrete.

          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 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.isOpenEmbedding_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 : Topology.IsOpenEmbedding (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.