Theorems · Theorem · algebraic topology

IsClosedMap.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], IsClosedMap f → (∀ x ∈ s, (f ⁻¹' {x}).Finite) → IsLocalHomeomorphOn f (f ⁻¹' s) → IsCoveringMapOn f s

If f : E → X is a closed map between topological spaces with E Hausdorff, and s is a subset of X on which f has finite fibers, such that f restricts to a homeomorphism on a neighborhood of every point of f ⁻¹' s, then f is a covering map on s.

Defined in

Mathlib.Topology.Covering.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceT2Space