Pulling a covering back to an evenly covered open set gives a trivial covering

Given: The objects, hypotheses, and choice principles stated above.

For a covering $p:E\to B$ and a continuous map $f:X\to B$, define $f^{\ast }E:=\{(x,e)\in X\times E:f(x)=p(e)\}$ with the subspace topology, and let $f^{\ast }p:f^{\ast }E\to X$ be $(x,e)\mapsto x$ (def-product-topology, def-subspace-topology-top). This is the pullback covering space; its covering property is proved in prop-covering-spaces-are-stable-under-restriction-finite-products-and-pullback. (The pullback of a covering space along a continuous map).

A covering map is a continuous surjection $p:E\to B$ such that every $b\in B$ has an open neighbourhood $U$ for which $p^{-1}(U)$ is a disjoint union of open sets $V_j$, called sheets, and each restriction $p{\mathrm{\mid }}_{V_j}:V_j\to U$ is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a $U$ is evenly covered, and $p^{-1}(b)$ is the fibre over $b$. A covering is trivial when it is isomorphic over $B$ to a product projection $B\times F\to B$ with $F$ discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

If $X$ is any space and $F$ is a nonempty discrete space, the projection $X\times F\to X$ is a trivial covering with fibre $F$. If $X=\mathrm{\varnothing }$, the same holds for $F=\mathrm{\varnothing }$; for nonempty $X$, an empty fibre would violate surjectivity. (Trivial coverings are products with a discrete fibre).