[proofplan] Uniqueness is immediate from [Uniqueness of Lifts](/theorems/1885) on the connected space $Y$. The forward direction is functoriality: if $\tilde{f} = p \circ \tilde{f}$ exists then $f_* = p_* \circ \tilde{f}_*$ factors through $p_*$, placing $\operatorname{image}(f_*) \subseteq \operatorname{image}(p_*)$. For the backward direction, we construct $\tilde{f}$ by "path chasing": for $y \in Y$, pick a path $\alpha_y$ from $y_0$ to $y$, push it down to a path $f \circ \alpha_y$ in $X$ from $x_0$, lift that path to $\tilde{X}$ starting at $\tilde{x}_0$ via the [Path Lifting Lemma](/theorems/1886), and define $\tilde{f}(y)$ to be its endpoint. The algebraic hypothesis $f_*\pi_1(Y, y_0) \leq p_*\pi_1(\tilde{X}, \tilde{x}_0)$ is consumed exactly to guarantee path-independence of $\tilde{f}(y)$. Continuity uses local path-connectedness of $Y$ to express $\tilde{f}$ locally as $(p|_{\tilde{V}})^{-1} \circ f$ on small path-connected opens, which is continuous. [/proofplan] [step:Prove uniqueness from connectedness of $Y$] Suppose $\tilde{f}_1, \tilde{f}_2: Y \to \tilde{X}$ are two continuous lifts of $f$ with $\tilde{f}_1(y_0) = \tilde{f}_2(y_0) = \tilde{x}_0$. Since $Y$ is path-connected it is in particular connected, and [Uniqueness of Lifts](/theorems/1885) applied to the covering $p: \tilde{X} \to X$, the connected space $Y$, the map $f: Y \to X$, and the two lifts $\tilde{f}_1, \tilde{f}_2$ agreeing at the single point $y_0$, forces $\tilde{f}_1 = \tilde{f}_2$ on all of $Y$. [guided] We establish uniqueness before we begin the existence argument, because uniqueness is a much shorter and entirely independent fact. Suppose we had two continuous lifts $\tilde{f}_1, \tilde{f}_2: Y \to \tilde{X}$ of the same continuous $f: Y \to X$ along the same covering $p: \tilde{X} \to X$, both with $\tilde{f}_1(y_0) = \tilde{f}_2(y_0) = \tilde{x}_0$. We apply [Uniqueness of Lifts](/theorems/1885). That theorem requires: (i) $p: \tilde{X} \to X$ is a covering map — given in our hypotheses; (ii) $Y$ is connected — we have path-connected, which implies connected; (iii) $\tilde{f}_1, \tilde{f}_2: Y \to \tilde{X}$ are continuous with $p \circ \tilde{f}_1 = f = p \circ \tilde{f}_2$ — both are lifts by assumption; (iv) there is some point where $\tilde{f}_1$ and $\tilde{f}_2$ agree — they agree at $y_0$. The conclusion is $\tilde{f}_1 = \tilde{f}_2$ on all of $Y$. This proves the "uniqueness" statement in the theorem. We may assume from now on that we are constructing *the* lift if one exists. [/guided] [/step] [step:Prove the forward direction by functoriality] Suppose a continuous lift $\tilde{f}: (Y, y_0) \to (\tilde{X}, \tilde{x}_0)$ with $p \circ \tilde{f} = f$ exists. Applying the fundamental group functor ([Induced Homomorphism on Fundamental Groups](/theorems/1879)) to the based spaces $(Y, y_0), (\tilde{X}, \tilde{x}_0), (X, x_0)$ gives group homomorphisms \begin{align*} \tilde{f}_*: \pi_1(Y, y_0) &\to \pi_1(\tilde{X}, \tilde{x}_0), \\ p_*: \pi_1(\tilde{X}, \tilde{x}_0) &\to \pi_1(X, x_0), \\ f_*: \pi_1(Y, y_0) &\to \pi_1(X, x_0). \end{align*} By functoriality, \begin{align*} f_* = (p \circ \tilde{f})_* = p_* \circ \tilde{f}_*. \end{align*} Hence for any $[\gamma] \in \pi_1(Y, y_0)$, $f_*([\gamma]) = p_*(\tilde{f}_*([\gamma])) \in p_*\pi_1(\tilde{X}, \tilde{x}_0)$. Therefore \begin{align*} f_* \pi_1(Y, y_0) \subseteq p_* \pi_1(\tilde{X}, \tilde{x}_0). \end{align*} [guided] The forward direction says: if a lift exists, then the algebraic condition $f_*\pi_1(Y, y_0) \leq p_*\pi_1(\tilde{X}, \tilde{x}_0)$ holds. This is the "easy direction" — pure functoriality. Suppose $\tilde{f}: (Y, y_0) \to (\tilde{X}, \tilde{x}_0)$ is a continuous lift: $p \circ \tilde{f} = f$ and $\tilde{f}(y_0) = \tilde{x}_0$. Apply the fundamental group functor of [Induced Homomorphism on Fundamental Groups](/theorems/1879) to each of the three maps: \begin{align*} \tilde{f}_* &: \pi_1(Y, y_0) \to \pi_1(\tilde{X}, \tilde{x}_0), & [\gamma] \mapsto [\tilde{f} \circ \gamma], \\ p_* &: \pi_1(\tilde{X}, \tilde{x}_0) \to \pi_1(X, x_0), & [\tilde{\delta}] \mapsto [p \circ \tilde{\delta}], \\ f_* &: \pi_1(Y, y_0) \to \pi_1(X, x_0), & [\gamma] \mapsto [f \circ \gamma]. \end{align*} The **composition law** for the functor (see [Induced Homomorphism on Fundamental Groups](/theorems/1879)) gives $(p \circ \tilde{f})_* = p_* \circ \tilde{f}_*$. Combined with $p \circ \tilde{f} = f$ we get \begin{align*} f_* = p_* \circ \tilde{f}_*. \end{align*} Hence, given any $[\gamma] \in \pi_1(Y, y_0)$, \begin{align*} f_*[\gamma] = p_*(\tilde{f}_* [\gamma]) \in p_* \pi_1(\tilde{X}, \tilde{x}_0). \end{align*} Since this holds for every $[\gamma]$, the image of $f_*$ is contained in the image of $p_*$: \begin{align*} f_*\pi_1(Y, y_0) \subseteq p_*\pi_1(\tilde{X}, \tilde{x}_0), \end{align*} as subgroups of $\pi_1(X, x_0)$. This is the required inclusion. [/guided] [/step] [step:Set up the pointwise construction of the lift] We now prove the backward direction. Suppose $f_*\pi_1(Y, y_0) \leq p_*\pi_1(\tilde{X}, \tilde{x}_0)$. For each $y \in Y$, pick a path $\alpha_y: I \to Y$ with $\alpha_y(0) = y_0, \alpha_y(1) = y$ (exists by path-connectedness of $Y$). The composition $f \circ \alpha_y: I \to X$ is a path starting at $f(y_0) = x_0$. By the [Path Lifting Lemma](/theorems/1886) applied to the covering $p$ and the initial point $\tilde{x}_0 \in p^{-1}(x_0)$, there is a unique lift \begin{align*} \widetilde{f \circ \alpha_y}: I \to \tilde{X}, \qquad \widetilde{f \circ \alpha_y}(0) = \tilde{x}_0, \quad p \circ \widetilde{f \circ \alpha_y} = f \circ \alpha_y. \end{align*} Tentatively define \begin{align*} \tilde{f}(y) := \widetilde{f \circ \alpha_y}(1). \end{align*} Note $p(\tilde{f}(y)) = (f \circ \alpha_y)(1) = f(y)$ by construction, so $\tilde{f}$ is a **set-theoretic** lift of $f$. The three remaining tasks are (i) show $\tilde{f}(y)$ is independent of the choice of $\alpha_y$, (ii) verify $\tilde{f}(y_0) = \tilde{x}_0$, (iii) show $\tilde{f}$ is continuous. For (ii): take $\alpha_{y_0} = c_{y_0}$ the constant path at $y_0$. Then $f \circ \alpha_{y_0} = c_{x_0}$, and its lift starting at $\tilde{x}_0$ is the constant path $c_{\tilde{x}_0}$ (by [Uniqueness of Lifts](/theorems/1885), constants lift to constants). Hence $\tilde{f}(y_0) = c_{\tilde{x}_0}(1) = \tilde{x}_0$. [guided] Now for the existence direction. We have the algebraic condition $f_*\pi_1(Y, y_0) \subseteq p_*\pi_1(\tilde{X}, \tilde{x}_0)$ and want to build $\tilde{f}$. **Strategy.** For each $y \in Y$, any path from $y_0$ to $y$ pushes down to a path in $X$ from $x_0$ to $f(y)$, which can be lifted to $\tilde{X}$ starting at $\tilde{x}_0$; we define $\tilde{f}(y)$ to be the endpoint of the lifted path. **Pointwise definition.** Fix $y \in Y$. By path-connectedness of $Y$, choose a path \begin{align*} \alpha_y: I \to Y, \qquad \alpha_y(0) = y_0, \qquad \alpha_y(1) = y. \end{align*} Compose with $f$ to obtain a path in $X$: \begin{align*} f \circ \alpha_y: I \to X, \qquad (f \circ \alpha_y)(0) = f(y_0) = x_0, \qquad (f \circ \alpha_y)(1) = f(y). \end{align*} By the [Path Lifting Lemma](/theorems/1886) applied to the covering $p: \tilde{X} \to X$, the path $f \circ \alpha_y$, and the initial point $\tilde{x}_0 \in p^{-1}(x_0)$, there is a unique lift $\widetilde{f \circ \alpha_y}: I \to \tilde{X}$ with $\widetilde{f \circ \alpha_y}(0) = \tilde{x}_0$ and $p \circ \widetilde{f \circ \alpha_y} = f \circ \alpha_y$. Tentatively set \begin{align*} \tilde{f}(y) := \widetilde{f \circ \alpha_y}(1) \in \tilde{X}. \end{align*} **Sanity checks.** 1. $p(\tilde{f}(y)) = p(\widetilde{f \circ \alpha_y}(1)) = (f \circ \alpha_y)(1) = f(y)$. So $\tilde{f}$ is a *set-theoretic* lift of $f$, whatever else may be. 2. At the basepoint $y = y_0$, we may take $\alpha_{y_0} = c_{y_0}$ constant. Then $f \circ c_{y_0} = c_{x_0}$ is constant in $X$, and the constant $c_{\tilde{x}_0}$ is a lift starting at $\tilde{x}_0$; by [Uniqueness of Lifts](/theorems/1885), it *is* the unique lift. So $\tilde{f}(y_0) = c_{\tilde{x}_0}(1) = \tilde{x}_0$, matching the required initial condition. **Still to prove.** The candidate $\tilde{f}(y)$ was defined using a choice of $\alpha_y$. We must show the endpoint $\widetilde{f \circ \alpha_y}(1)$ is independent of that choice — otherwise $\tilde{f}$ is not a function. After well-definedness, we must prove continuity. [/guided] [/step] [step:Verify well-definedness using the algebraic hypothesis] Let $\alpha_y, \alpha'_y: I \to Y$ be two paths from $y_0$ to $y$. Let $\ell_1, \ell_2: I \to \tilde{X}$ be the unique lifts of $f \circ \alpha_y$ and $f \circ \alpha'_y$ starting at $\tilde{x}_0$, respectively. We must show $\ell_1(1) = \ell_2(1)$. Form the loop $\gamma := \alpha'_y \cdot \overline{\alpha_y}$ in $Y$ at $y_0$, where $\overline{\alpha_y}(t) := \alpha_y(1 - t)$ is the reverse path. Then $[\gamma] \in \pi_1(Y, y_0)$, and $f \circ \gamma = (f \circ \alpha'_y) \cdot \overline{(f \circ \alpha_y)}$ is a loop in $X$ at $x_0$ representing $f_*[\gamma]$. By hypothesis, \begin{align*} f_*[\gamma] \in f_*\pi_1(Y, y_0) \subseteq p_*\pi_1(\tilde{X}, \tilde{x}_0), \end{align*} so there exists $[\tilde{\delta}] \in \pi_1(\tilde{X}, \tilde{x}_0)$ with $p_*[\tilde{\delta}] = f_*[\gamma]$, i.e. $p \circ \tilde{\delta} \simeq f \circ \gamma$ rel endpoints in $X$. In particular, the loop $f \circ \gamma$ is path-homotopic rel endpoints to $p \circ \tilde{\delta}$, hence the unique lift of $f \circ \gamma$ starting at $\tilde{x}_0$ has the same terminal point as the unique lift of $p \circ \tilde{\delta}$ starting at $\tilde{x}_0$, by [Lifted Path Homotopy](/theorems/1888). The unique lift of $p \circ \tilde{\delta}$ starting at $\tilde{x}_0$ is $\tilde{\delta}$ itself (by [Uniqueness of Lifts](/theorems/1885)), which is a **loop** at $\tilde{x}_0$, ending at $\tilde{x}_0$. Hence the lift of $f \circ \gamma$ starting at $\tilde{x}_0$ is also a loop at $\tilde{x}_0$. On the other hand, the lift of $f \circ \gamma = (f \circ \alpha'_y) \cdot \overline{(f \circ \alpha_y)}$ starting at $\tilde{x}_0$ can be constructed piecewise: first lift $f \circ \alpha'_y$ from $\tilde{x}_0$ to get $\ell_2$ ending at $\ell_2(1)$, then lift $\overline{f \circ \alpha_y}$ starting at $\ell_2(1)$. Now $\overline{f \circ \alpha_y}$ is the reverse of $f \circ \alpha_y$; and the lift of $f \circ \alpha_y$ starting at $\tilde{x}_0$ is $\ell_1$ ending at $\ell_1(1)$. By [Uniqueness of Lifts](/theorems/1885) applied to the reverse, the lift of $\overline{f \circ \alpha_y}$ ending at $\tilde{x}_0$ is $\overline{\ell_1}$; traversed forward, this lift *starts* at $\ell_1(1)$. So the lift of $\overline{f \circ \alpha_y}$ starting at $\ell_2(1)$ exists and is unique (again [Path Lifting Lemma](/theorems/1886)), with terminal point determined by $\ell_2(1)$; for this lifted concatenation to be a loop ending at $\tilde{x}_0$, one needs $\ell_2(1) = \ell_1(1)$ (so that starting the reverse lift from there delivers the unique continuation $\overline{\ell_1}$ ending at $\tilde{x}_0$). Explicitly: the concatenation-lift starting at $\tilde{x}_0$ passes through $\ell_2(1)$ at $t = 1/2$, then proceeds along the unique lift of $\overline{f \circ \alpha_y}$ starting from $\ell_2(1)$. This concatenation is a loop at $\tilde{x}_0$ iff the reverse-lift terminates at $\tilde{x}_0$, iff its forward-time lift (as the reverse of the reverse) starts at $\tilde{x}_0$ — which is the lift of $f \circ \alpha_y$ starting at $\tilde{x}_0$, namely $\ell_1$. Uniqueness of lifts forces $\ell_2(1)$ to be $\ell_1(1)$, otherwise the two lifts of $f \circ \alpha_y$ from $\tilde{x}_0$ (the one built by reversal here and $\ell_1$) would differ. Hence $\ell_1(1) = \ell_2(1)$, and $\tilde{f}(y)$ is independent of the choice of $\alpha_y$. [guided] This is the crucial step — where the algebraic hypothesis earns its keep. We check that the endpoint of the lifted path does not depend on which path $\alpha_y$ we chose in $Y$ from $y_0$ to $y$. **Setting up the comparison.** Let $\alpha_y$ and $\alpha'_y$ be two paths in $Y$ from $y_0$ to $y$. Let $\ell_1$ be the unique lift of $f \circ \alpha_y$ starting at $\tilde{x}_0$, and $\ell_2$ the unique lift of $f \circ \alpha'_y$ starting at $\tilde{x}_0$. We want to show $\ell_1(1) = \ell_2(1)$. **Concatenate into a loop.** Form \begin{align*} \gamma := \alpha'_y \cdot \overline{\alpha_y}: I \to Y. \end{align*} Since $\alpha'_y(0) = y_0, \alpha'_y(1) = y = \overline{\alpha_y}(0), \overline{\alpha_y}(1) = y_0$, $\gamma$ is a loop at $y_0$, so $[\gamma] \in \pi_1(Y, y_0)$. **Consume the hypothesis.** By assumption $f_*\pi_1(Y, y_0) \subseteq p_*\pi_1(\tilde{X}, \tilde{x}_0)$, so $f_*[\gamma] \in p_*\pi_1(\tilde{X}, \tilde{x}_0)$. By definition of $p_*$, there exists a loop $\tilde{\delta}$ in $\tilde{X}$ at $\tilde{x}_0$ with $[p \circ \tilde{\delta}] = [f \circ \gamma]$ in $\pi_1(X, x_0)$, i.e. $p \circ \tilde{\delta} \simeq f \circ \gamma$ rel endpoints. **Lift the loop $f \circ \gamma$.** Let $\tilde{\gamma}^*$ be the unique lift of $f \circ \gamma$ starting at $\tilde{x}_0$. Apply [Lifted Path Homotopy](/theorems/1888) to the path-homotopy $p \circ \tilde{\delta} \simeq f \circ \gamma$: the lifts of homotopic paths rel endpoints, starting at the same point, are themselves homotopic rel endpoints — hence share their terminal point. The lift of $p \circ \tilde{\delta}$ starting at $\tilde{x}_0$ is $\tilde{\delta}$ itself (by [Uniqueness of Lifts](/theorems/1885)), and $\tilde{\delta}$ is a loop at $\tilde{x}_0$, so $\tilde{\delta}(1) = \tilde{x}_0$. Therefore $\tilde{\gamma}^*(1) = \tilde{x}_0$, i.e. $\tilde{\gamma}^*$ is also a loop at $\tilde{x}_0$. **Decompose the lifted loop.** The loop $f \circ \gamma$ is the concatenation $(f \circ \alpha'_y) \cdot \overline{(f \circ \alpha_y)}$. Its lift starting at $\tilde{x}_0$ is obtained by concatenating \begin{align*} \tilde{\gamma}^* = \ell_2 \cdot \tilde{\mu}, \end{align*} where $\ell_2$ is the lift of $f \circ \alpha'_y$ from $\tilde{x}_0$ (unique by [Path Lifting Lemma](/theorems/1886) and [Uniqueness of Lifts](/theorems/1885)), and $\tilde{\mu}$ is the unique lift of $\overline{f \circ \alpha_y}$ starting from $\ell_2(1)$. **Identify $\tilde{\mu}$.** Reversing, $\overline{\tilde{\mu}}$ is a lift of $f \circ \alpha_y$ starting from $\tilde{\mu}(1)$ and ending at $\ell_2(1)$. Alternatively, $\overline{\tilde{\mu}}$ is a lift of $f \circ \alpha_y$ whose terminal point is $\ell_2(1)$. **Force $\ell_1(1) = \ell_2(1)$.** We know $\tilde{\gamma}^*(1) = \tilde{x}_0$, and $\tilde{\gamma}^*(1) = \tilde{\mu}(1)$. So $\tilde{\mu}(1) = \tilde{x}_0$, i.e. $\overline{\tilde{\mu}}(0) = \tilde{x}_0$. Thus $\overline{\tilde{\mu}}$ is a lift of $f \circ \alpha_y$ starting at $\tilde{x}_0$. By uniqueness of lifts (the [Path Lifting Lemma](/theorems/1886) gives existence; [Uniqueness of Lifts](/theorems/1885) gives uniqueness), $\overline{\tilde{\mu}} = \ell_1$. Hence \begin{align*} \ell_1(1) = \overline{\tilde{\mu}}(1) = \tilde{\mu}(0) = \ell_2(1), \end{align*} as claimed. This establishes that $\tilde{f}(y) := \widetilde{f \circ \alpha_y}(1)$ is a **well-defined** function of $y$, independent of the choice of $\alpha_y$. The hypothesis $f_*\pi_1(Y, y_0) \leq p_*\pi_1(\tilde{X}, \tilde{x}_0)$ was consumed exactly once, at the step where we used $f_*[\gamma] \in p_*\pi_1(\tilde{X}, \tilde{x}_0)$ to promote the projected loop to an element that lifts to a loop. [/guided] [/step] [step:Prove continuity of $\tilde{f}$ using local path-connectedness of $Y$] Fix $y \in Y$. Set $x = f(y) \in X$ and $\tilde{x} = \tilde{f}(y) \in \tilde{X}$, so $p(\tilde{x}) = x$. Let $\tilde{N}$ be an open neighbourhood of $\tilde{x}$ in $\tilde{X}$. Since $p: \tilde{X} \to X$ is a covering map, pick an evenly covered open $V \subseteq X$ containing $x$: $p^{-1}(V) = \bigsqcup_j \tilde{V}_j$ with each $p|_{\tilde{V}_j}: \tilde{V}_j \to V$ a homeomorphism. Let $\tilde{V}$ be the sheet containing $\tilde{x}$. Shrink $\tilde{V}$ to $\tilde{V} \cap \tilde{N}$ (still a neighbourhood of $\tilde{x}$, mapped homeomorphically onto an open $V' := p(\tilde{V} \cap \tilde{N})$ in $V$). So without loss we may assume $\tilde{V} \subseteq \tilde{N}$ and $p|_{\tilde{V}}: \tilde{V} \to V$ is a homeomorphism. By continuity of $f$, the preimage $f^{-1}(V)$ is open in $Y$ and contains $y$. By local path-connectedness of $Y$, there is a path-connected open $W \subseteq f^{-1}(V)$ with $y \in W$. Claim: for every $z \in W$, $\tilde{f}(z) \in \tilde{V} \subseteq \tilde{N}$. *Proof.* Pick a path $\beta: I \to W$ with $\beta(0) = y$ and $\beta(1) = z$. Since $W \subseteq f^{-1}(V)$, the path $f \circ \beta: I \to V$ lies in $V$. Let $\tilde{\beta} := (p|_{\tilde{V}})^{-1} \circ f \circ \beta: I \to \tilde{V}$, which is continuous because $p|_{\tilde{V}}^{-1}$ is a homeomorphism. Then $p \circ \tilde{\beta} = f \circ \beta$ and $\tilde{\beta}(0) = (p|_{\tilde{V}})^{-1}(f(y)) = (p|_{\tilde{V}})^{-1}(x) = \tilde{x} = \tilde{f}(y)$. So $\tilde{\beta}$ is a lift of $f \circ \beta$ starting at $\tilde{f}(y)$; by [Uniqueness of Lifts](/theorems/1885), it is the unique such lift. Now choose the path $\alpha_z$ for the definition of $\tilde{f}(z)$ to be $\alpha_y \cdot \beta$ (concatenating a reference path $\alpha_y$ from $y_0$ to $y$ with the small path $\beta$ from $y$ to $z$); this is a path in $Y$ from $y_0$ to $z$. By well-definedness (Step 4), $\tilde{f}(z)$ equals the endpoint of the lift of $f \circ \alpha_z = (f \circ \alpha_y) \cdot (f \circ \beta)$ starting at $\tilde{x}_0$. This lift is obtained by first lifting $f \circ \alpha_y$ from $\tilde{x}_0$ — endpoint $\widetilde{f \circ \alpha_y}(1) = \tilde{f}(y) = \tilde{x}$ — then lifting $f \circ \beta$ from $\tilde{x}$, which by the preceding paragraph gives $\tilde{\beta}$ ending at $(p|_{\tilde{V}})^{-1}(f(z))$. Hence \begin{align*} \tilde{f}(z) = (p|_{\tilde{V}})^{-1}(f(z)) \in \tilde{V} \subseteq \tilde{N}. \end{align*} Therefore $W \subseteq \tilde{f}^{-1}(\tilde{N})$, so $\tilde{f}^{-1}(\tilde{N})$ is a neighbourhood of $y$. As $y$ and $\tilde{N}$ were arbitrary, $\tilde{f}$ is continuous. Since $\tilde{f}$ is continuous, $\tilde{f}(y_0) = \tilde{x}_0$ (Step 3), and $p \circ \tilde{f} = f$ (Step 3), $\tilde{f}$ is a based continuous lift of $f$. This completes the backward direction. [guided] The last task is continuity of $\tilde{f}$. The hypothesis on $Y$ being **locally path-connected** is consumed here — it lets us propagate the local inverse $(p|_{\tilde{V}})^{-1}$ along small neighbourhoods in $Y$. **Setup.** Fix $y \in Y$ and a neighbourhood $\tilde{N}$ of $\tilde{f}(y)$ in $\tilde{X}$. We must find a neighbourhood $W$ of $y$ in $Y$ with $\tilde{f}(W) \subseteq \tilde{N}$. **Shrink to an evenly covered sheet.** Since $p$ is a covering, pick $V \subseteq X$ open, evenly covered, with $f(y) \in V$: write $p^{-1}(V) = \bigsqcup_j \tilde{V}_j$ with $p|_{\tilde{V}_j}: \tilde{V}_j \to V$ a homeomorphism. Let $\tilde{V}$ be the sheet containing $\tilde{f}(y)$. By shrinking, we may assume $\tilde{V} \subseteq \tilde{N}$: take $\tilde{V}' := \tilde{V} \cap \tilde{N}$, which is open in $\tilde{V}$ hence open in $\tilde{X}$, with $\tilde{f}(y) \in \tilde{V}'$; its image $V' := p(\tilde{V}')$ is open in $V$ (homeomorphic image of an open set), still contains $f(y)$, and still evenly covered with $\tilde{V}'$ the sheet over it. Replace $V, \tilde{V}$ by $V', \tilde{V}'$. **Local path-connected neighbourhood.** By continuity of $f$, $f^{-1}(V)$ is open in $Y$ and contains $y$. By local path-connectedness of $Y$, $y$ has a path-connected open neighbourhood $W$ contained in $f^{-1}(V)$. This is exactly where local path-connectedness is consumed. **Evaluate $\tilde{f}$ on $W$.** Let $z \in W$. Pick a path $\beta: I \to W$ from $y$ to $z$ (exists since $W$ is path-connected). Push down: $f \circ \beta: I \to V$ is a path from $f(y)$ to $f(z)$ staying in $V$. Since $p|_{\tilde{V}}: \tilde{V} \to V$ is a homeomorphism, define \begin{align*} \tilde{\beta} := (p|_{\tilde{V}})^{-1} \circ f \circ \beta: I \to \tilde{V}. \end{align*} Continuity is immediate; $p \circ \tilde{\beta} = f \circ \beta$; and $\tilde{\beta}(0) = (p|_{\tilde{V}})^{-1}(f(y)) = \tilde{f}(y)$ (since $\tilde{f}(y)$ is in $\tilde{V}$ and lifts $f(y)$). So $\tilde{\beta}$ is the unique lift of $f \circ \beta$ starting at $\tilde{f}(y)$ (uniqueness from [Uniqueness of Lifts](/theorems/1885)). **Use well-definedness.** Let $\alpha_y$ be a reference path from $y_0$ to $y$. Then $\alpha_z := \alpha_y \cdot \beta$ is a path in $Y$ from $y_0$ to $z$. By Step 4, $\tilde{f}(z)$ is the endpoint of the unique lift of $f \circ \alpha_z$ starting at $\tilde{x}_0$. We construct that lift piecewise: first lift $f \circ \alpha_y$ from $\tilde{x}_0$, reaching $\tilde{f}(y)$ at $t = 1/2$ (after reparametrisation); then lift $f \circ \beta$ from $\tilde{f}(y)$, reaching $\tilde{\beta}(1) = (p|_{\tilde{V}})^{-1}(f(z))$ at $t = 1$. Hence \begin{align*} \tilde{f}(z) = (p|_{\tilde{V}})^{-1}(f(z)) \in \tilde{V} \subseteq \tilde{N}. \end{align*} **Punchline.** This shows $\tilde{f}(W) \subseteq \tilde{N}$, so $W \subseteq \tilde{f}^{-1}(\tilde{N})$ and $\tilde{f}^{-1}(\tilde{N})$ is a neighbourhood of $y$. Since $y$ and $\tilde{N}$ were arbitrary, $\tilde{f}$ is continuous. On the neighbourhood $W$, the formula $\tilde{f}|_W = (p|_{\tilde{V}})^{-1} \circ f|_W$ holds exactly: both sides are continuous lifts of $f|_W$ starting at the same point $\tilde{f}(y)$, hence agree on the path-connected domain $W$ by [Uniqueness of Lifts](/theorems/1885). [/guided] [/step] [step:Assemble: uniqueness, necessity, sufficiency] Step 1 establishes uniqueness of the lift (whenever it exists) from connectedness of $Y$. Step 2 establishes the forward direction: if a lift exists, then $f_*\pi_1(Y, y_0) \leq p_*\pi_1(\tilde{X}, \tilde{x}_0)$. Steps 3-5 establish the backward direction: given the algebraic containment, the map $\tilde{f}$ constructed pointwise by path-chasing is a well-defined, basepoint-preserving, continuous lift. Together these give the equivalence claimed in the theorem, with uniqueness established. This completes the proof. [/step]