Theorems · Definition · algebraic topology

IsCoveringMap

{E : Type u_1} → {X : Type u_2} → [TopologicalSpace E] → [TopologicalSpace X] → (E → X) → Prop

A covering map is a continuous function f : E → X with discrete fibers such that each point of X has an evenly covered neighborhood.

Defined in

Mathlib.Topology.Covering.Basic

Cited by

68 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace