4.2.1. Locally trivial maps with discrete fibers.🔗

If f : E → X is locally trivial with discrete fibers then the lemma IsFiberBundle.isCoveringMap demonstrates that f is a covering map. This uses the same definition Bundle.Trivialization as Mathlib's fiber bundle theory.

An convenience variant of this also exists as FiberBundle.isCoveringMap in which the FiberBundle definition is used.

4.2.2. Closed local homeomorphisms with finite fibers🔗

If E is Hausdorff, a sufficient condition for f : E → X to be a covering map is that it is a closed, local homeomorphism, with finite fibers. Mathlib knows this fact as IsClosedMap.isCoveringMapOn_of_isLocalHomeomorphOn.

4.2.3. Local homeomorphims from a compact space🔗

If E is compact and Hausdorff and X is Hausdorff, then a map f : E → X is a local homeomorphism iff it is a covering map. Mathlib knows this fact as isLocalHomeomorph_iff_isCoveringMap.