Existence and uniqueness of path lifts through a covering map

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

Let $p:E\to B$ be a covering and $f:Y\to B$ continuous. A lift of $f$ through $p$ is a continuous map $\tilde{f}:Y\to E$ with $p\circ \tilde{f}=f$. This includes lifts of paths $I\to B$ and of homotopies $Y\times I\to B$; an initial lift prescribes the restriction at time $0$ (def-homotopy-relative-and-path-homotopy, def-path-connected). (Lifts of maps, paths, and homotopies through a covering map).

Let $(X,d)$ be a compact metric space (def-metric-compactness, def-metric-space) and let $\mathcal{U}$ be an open cover of $X$. Then there is a real $\delta >0$, a Lebesgue number for $\mathcal{U}$, such that every nonempty $A\subseteq X$ with $\mathrm{diam}(A)<\delta$ (def-metric-bounded-diameter) satisfies $A\subseteq U$ for some $U\in \mathcal{U}$. Diameters of nonempty subsets of $X$ are defined because a compact space is bounded (thm-compact-subset-is-closed-and-bounded) and a subset of a bounded set is bounded. No choice principle is used. (Every open cover of a compact metric space has a Lebesgue number: a $\delta >0$ such that every nonempty subset of diameter less than $\delta$ lies inside a single member of the cover).

Let $X$, $Y$ and $Z$ be topological spaces, with subspaces carrying the subspace topology (def-subspace-topology-top). Then: 1. Composites. If $f:X\to Y$ and $g:Y\to Z$ are continuous (def-continuous-map-top) then $g\circ f:X\to Z$ is continuous. 2. Open cover. Let $f:X\to Y$ be a function and let $\{U_i:i\in I\}$ be a family of open subsets of $X$ with ${\bigcup }_{i\in I}{U}_i=X$. If $f{\mathrm{\mid }}_{U_i}:U_i\to Y$ is continuous for every $i\in I$, then $f$ is continuous. 3. Finite closed cover. Let $f:X\to Y$ be a function, let $n\ge 1$ and let $F_1,\dots ,F_n$ be closed subsets of $X$ with $F_1\cup \cdots \cup F_n=X$. If $f{\mathrm{\mid }}_{F_k}:F_k\to Y$ is continuous for every $k$, then $f$ is continuous. The converses of claims 2 and 3 hold with no hypothesis on the cover at all: every restriction of a continuous map to a subspace is continuous (def-subspace-topology-top). The finiteness in claim 3 is not removable; see the remarks. (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).

Let $(X,\mathcal{T})$ be a topological space (def-topological-space). An open cover of $(X,\mathcal{T})$ is a family $\mathcal{U}\subseteq \mathcal{T}$ of open sets with $X=\bigcup \mathcal{U}$; a subcover of $\mathcal{U}$ is a subfamily that is itself an open cover; and $(X,\mathcal{T})$ is compact when every open cover of it has a finite subcover. (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

Every point of $B$ has an evenly covered open neighbourhood $U$: $p^{-1}(U)$ is a disjoint union of open sheets $V$, and $p{\mathrm{\mid }}_V:V\to U$ is a homeomorphism. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

The closed interval $I=[0,1]$ is compact in the usual metric, and every closed subinterval of $I$ is connected. (Heine-Borel in ${\mathbb{R}}^n$: with the Euclidean metric a subset of ${\mathbb{R}}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, A subset of $\mathbb{R}$ is connected if and only if it is order-convex, that is, an interval).

For every real $x$ there is an integer $m\ge 1$ with $x<m$. (Every complete ordered field is Archimedean).