Two lifts from a connected space that agree at one point agree everywhere

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,\mathcal{T})$ be a topological space (def-topological-space). A separation of $X$ is an ordered pair $(U,V)$ of open, nonempty, disjoint subsets of $X$ with $U\cup V=X$; $X$ is disconnected when a separation of $X$ exists and connected when none does. Since $U$ and $V$ are complementary each is clopen, so a separation is the same thing as a partition of $X$ into two nonempty clopen pieces. A subset $A\subseteq X$ is a connected subset when the subspace $(A,{\mathcal{T}}_A)$ is connected. (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).

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