Theorems · Theorem · algebraic topology

IsCoveringMapOn.of_isLocalHomeomorphOn

∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {s : Set X}
  [T2Space E] [T2Space X] [CompactSpace E], Continuous f → IsLocalHomeomorphOn f (f ⁻¹' s) → IsCoveringMapOn f s

If f : E → X is a continuous map between Hausdorff spaces with E compact, s is a subset of X such that f restricts to a homeomorphism on a neighborhood of every point of f ⁻¹' s, then f is a covering map on s. For example, s can be taken to be the set of regular values of a C¹ map f : E → X where E and X are manifolds of the same dimension with E compact, according to the inverse function theorem (see ContDiffAt.toOpenPartialHomeomorph).

Defined in

Mathlib.Topology.Covering.Basic

Cited by

2 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceT2SpaceT2SpaceCompactSpace