Covering maps are surjective local homeomorphisms with discrete fibres

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

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).

Let $(X,{\mathcal{T}}_X)$ and $(Y,{\mathcal{T}}_Y)$ be topological spaces and let $f:X\to Y$ be a function. Continuity is as in def-continuous-map-top, injections, surjections and bijections as in def-injection-surjection-bijection. $f$ is an open map if $f[U]$ is open in $Y$ for every open $U\subseteq X$, a closed map if $f[F]$ is closed in $Y$ for every closed $F\subseteq X$, and a homeomorphism if $f$ is a continuous bijection whose inverse $f^{-1}:Y\to X$ is also continuous; the spaces are homeomorphic when such an $f$ exists. (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).

Throughout, a topology is as in def-topological-space, and finite, at most countable and uncountable are as in def-countable, so that "countable" always means "at most countable" and every finite set is countable. Let $X$ be a set. The six families below are topologies on $X$; that each really satisfies (T1), (T2) and (T3) is discharged in full after the list. Among those six is the discrete topology ${\mathcal{T}}_{\mathrm{d}\mathrm{i}\mathrm{s}\mathrm{c}}:=\mathcal{P}(X)$, in which every subset is open and hence every subset is also closed. (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies).