4.1. Basic setup🔗

The following code expresses the fact that a map f : E → X between topological spaces is a covering map:

variable (E X : Type*)
  [TopologicalSpace E] [TopologicalSpace X]
  (f : E → X) (hf : IsCoveringMap f)

We may witness that this is defined using the expected property IsEvenlyCovered as follows:

example {g : E → X} :
    IsCoveringMap g ↔
      ∀ x, IsEvenlyCovered g x (g ⁻¹' {x}) :=
  Iff.rfl

Mathlib knows numerous facts about covering maps, including that they are:

Continuous: IsCoveringMap.continuous
Open: IsCoveringMap.isOpenMap
Local homeomorphisms: IsCoveringMap.isLocalHomeomorph
Quotient maps: IsCoveringMap.isQuotientMap
Separated maps: IsCoveringMap.isSeparatedMap

Mathlib also has API to support the situation when a map is only a covering map over some subset of the the base (this allows support for branched coverings). This is captured in IsCoveringMapOn and the related API.