[proofplan] The conclusion is a corollary of [Local Isometry from Complete Manifold is a Covering Map](/theorems/2735), whose hypotheses are weaker: a smooth surjective local diffeomorphism $f : M \to N$ from a complete $M$ satisfying $|df_p(v)|_h \geq |v|_g$ everywhere is a covering map. A local isometry $f : (M, g) \to (N, h)$ satisfies the metric inequality with equality $|df_p(v)|_h = |v|_g$, so it remains to verify surjectivity. We show $f(M) \subseteq N$ is both closed (using completeness of $M$ to upgrade Cauchy image-sequences to convergent ones) and open (using the local-diffeomorphism property of $f$). Connectedness of $N$ then forces $f(M) = N$. [/proofplan] [step:Verify the metric inequality and identify the regularity of $f$] Let $f : (M, g) \to (N, h)$ be a local isometry. By definition, for every $p \in M$ the differential $df_p : T_p M \to T_{f(p)} N$ is a linear isometry of inner product spaces, i.e., \begin{align*} h_{f(p)}(df_p(v), df_p(w)) = g_p(v, w) \quad \text{for all } v, w \in T_p M. \end{align*} In particular, $|df_p(v)|_h = |v|_g$ for every $v \in T_p M$, so the metric inequality $|df_p(v)|_h \geq |v|_g$ required by [Local Isometry from Complete Manifold is a Covering Map](/theorems/2735) holds with equality. Since $df_p$ is an isomorphism (an isometry between inner-product spaces of the same finite dimension is bijective), $f$ is a local diffeomorphism at every $p \in M$. Smoothness of $f$ is part of the local-isometry definition. Standing hypotheses going forward: $M$ is connected and complete, $N$ is connected, and $f : M \to N$ is a smooth local diffeomorphism with $|df_p(v)|_h = |v|_g$. [/step] [step:Show $f(M)$ is closed in $N$ via completeness of $M$] We show $f(M) \subseteq N$ is closed. Let $(q_n)_{n \geq 1} \subseteq f(M)$ converge to $q \in N$ (in the metric topology of $N$); we show $q \in f(M)$. Pick $p_n \in M$ with $f(p_n) = q_n$. We exhibit a preimage of $q$ explicitly by lifting short paths from $q_n$ to $q$, using completeness of $M$ to ensure the lifts extend to the full unit interval. Since $(q_n) \to q$ in $(N, d_h)$, choose $r_0 > 0$ such that $B_h(q, r_0) \subseteq N$ is a normal neighbourhood of $q$ in $(N, h)$ — i.e., $\exp_q^N : B_{T_q N}(0, r_0) \to B_h(q, r_0)$ is a diffeomorphism (such $r_0$ exists by [Exponential Map as a Local Diffeomorphism](/theorems/2712) applied at $q$ in $(N, h)$). Discarding finitely many terms, assume $q_n \in B_h(q, r_0)$ for all $n$. For each $n$, let $\beta_n : [0, 1] \to N$ be the unique radial $h$-geodesic with $\beta_n(0) = q_n$, $\beta_n(1) = q$; it has $h$-length $\ell_h(\beta_n) = d_h(q_n, q) < r_0$ and lies in $B_h(q, r_0)$. We lift $\beta_n$ to $M$ starting at $p_n$. The required path-lifting is the analytic core of [Local Isometry from Complete Manifold is a Covering Map](/theorems/2735), but we cannot invoke 2735 as a black box here because 2735 takes surjectivity of $f$ as a hypothesis, and surjectivity is precisely what we are proving. We therefore record the path-lifting result as an independent claim. [claim:Path-lifting for local isometries from a complete domain] Let $f : (M, g) \to (N, h)$ be a local isometry with $(M, g)$ complete, let $\beta : [0, 1] \to N$ be a smooth curve, and let $\tilde p \in f^{-1}(\beta(0))$. Then there exists a unique smooth curve $\tilde\beta : [0, 1] \to M$ with $\tilde\beta(0) = \tilde p$ and $f \circ \tilde\beta = \beta$. [/claim] [proof] Define $T := \sup\{t \in [0, 1] : \beta|_{[0, t]} \text{ has a smooth lift } \tilde\beta_t : [0, t] \to M \text{ with } \tilde\beta_t(0) = \tilde p\}$. Uniqueness follows from $f$ being a local diffeomorphism. **$T > 0$**: by the local-diffeomorphism property of $f$ at $\tilde p$, choose open $U \ni \tilde p$ with $f|_U : U \to f(U)$ a diffeomorphism, and $\delta > 0$ with $\beta([0, \delta]) \subseteq f(U)$; then $\tilde\beta := (f|_U)^{-1} \circ \beta|_{[0, \delta]}$ is a smooth lift on $[0, \delta]$. **Lift extends to $T$**: for $0 \leq s < t < T$, the local-isometry property gives $d_g(\tilde\beta(s), \tilde\beta(t)) \leq \ell_g(\tilde\beta|_{[s,t]}) = \ell_h(\beta|_{[s,t]})$. Uniform continuity of $\beta$ on $[0,1]$ makes $(\beta(t_k))$ Cauchy in $N$ for any $t_k \nearrow T$; the inequality transfers this to $(\tilde\beta(t_k))$ Cauchy in $(M, d_g)$. By completeness of $M$ via [Hopf–Rinow](/theorems/2726), $\tilde\beta(t_k) \to \tilde p_T$ for some $\tilde p_T \in M$, and continuity of $f$ gives $f(\tilde p_T) = \beta(T)$. Set $\tilde\beta(T) := \tilde p_T$; smoothness at $T$ follows from the local-diffeomorphism property of $f$ at $\tilde p_T$. **$T = 1$**: if $T < 1$, applying the $T > 0$ argument at $\tilde p_T$ extends the lift past $T$, contradicting maximality. [/proof] Applying the claim with $\beta = \beta_n$ and $\tilde p = p_n$, we obtain $\tilde\beta_n : [0, 1] \to M$ with $\tilde\beta_n(0) = p_n$ and $f \circ \tilde\beta_n = \beta_n$. Set $p_n^* := \tilde\beta_n(1) \in M$, so $f(p_n^*) = \beta_n(1) = q$. Hence $p_n^* \in f^{-1}(q)$, so $f^{-1}(q) \neq \varnothing$ and $q \in f(M)$. This shows every limit point of $f(M)$ in $N$ lies in $f(M)$, so $f(M)$ is closed in $N$. [guided] **The challenge.** We have $q_n \to q$ in $N$ with $q_n \in f(M)$, and we want $q \in f(M)$. We do not need to show that $(p_n)$ converges in $M$, and indeed it need not: with $M = \mathbb{R}$, $N = S^1$, $f(t) = e^{it}$, $q_n = e^{i/n} \to 1$, $p_n = 2\pi n + 1/n$ has no limit, yet $f^{-1}(1)$ is non-empty. **The strategy.** Construct a preimage of $q$ explicitly. Take a normal ball $B_h(q, r_0)$ around $q$ (supplied by [Exponential Map as a Local Diffeomorphism](/theorems/2712)). For $n$ large, $q_n \in B_h(q, r_0)$, and there is a unique radial $h$-geodesic $\beta_n$ from $q_n$ to $q$. Lift $\beta_n$ to $M$ starting at $p_n$; the endpoint $p_n^* := \tilde\beta_n(1)$ satisfies $f(p_n^*) = q$, so $p_n^* \in f^{-1}(q)$ and $q \in f(M)$. **Why path-lifting needs completeness.** The standard "open-closed-connected" lift on $[0,1]$ uses the local-diffeomorphism property of $f$ for openness, and completeness of $M$ via [Hopf–Rinow](/theorems/2726) for the closedness step (Cauchy lifts converge). Without completeness, the lift could escape to infinity in $M$ as $t \to T^-$. **Why we cannot black-box [theorem 2735](/theorems/2735).** Theorem 2735 takes *surjectivity* of $f$ as a hypothesis, which is precisely the conclusion of the present theorem. Citing 2735 to prove surjectivity would be circular. We extract the analytic core of 2735's proof — path-lifting from completeness — as a stand-alone claim. **Why exhibiting $p_n^*$ suffices.** Closedness of $f(M)$ requires only that $f^{-1}(q) \neq \varnothing$. The lift gives a preimage for free; we never need $(p_n)$ to converge. [/guided] [/step] [step:Show $f(M)$ is open in $N$ via the local-diffeomorphism property] We show $f(M)$ is open in $N$. Let $q \in f(M)$, and pick $p \in M$ with $f(p) = q$. By the local-diffeomorphism property of $f$ at $p$, there exists an open neighbourhood $U \subseteq M$ of $p$ such that $f|_U : U \to f(U) \subseteq N$ is a diffeomorphism with $f(U)$ open in $N$. Then $f(U) \subseteq f(M)$ is an open neighbourhood of $q = f(p)$ in $N$. Hence $q$ is an interior point of $f(M)$, and $f(M)$ is open. [/step] [step:Conclude $f(M) = N$ by connectedness, then apply the previous theorem] The set $f(M) \subseteq N$ is non-empty (contains $f(p)$ for any $p \in M$), open (Step 3), and closed (Step 2). Since $N$ is connected, $f(M)$ is a non-empty clopen subset, hence $f(M) = N$. This proves $f$ is surjective. We have established: - $f : M \to N$ is a smooth surjective local diffeomorphism (Step 1, plus surjectivity above), - $|df_p(v)|_h \geq |v|_g$ for all $p \in M$, $v \in T_p M$ (Step 1, with equality), - $M$ is complete (chapter hypothesis on $M$). By [Local Isometry from Complete Manifold is a Covering Map](/theorems/2735), $f$ is a covering map. The "in particular" surjectivity claim of the theorem is established directly above. [guided] The proof reduces to verifying the hypotheses of [Local Isometry from Complete Manifold is a Covering Map](/theorems/2735), which requires surjectivity. The surjectivity argument uses only that $f$ is a local diffeomorphism (for openness of $f(M)$) and that $M$ is complete plus the local-isometry property (for closedness of $f(M)$); connectedness of $N$ converts the clopen subset $f(M)$ into all of $N$. Why does completeness of $M$ enter the closedness step? Because we need to lift convergent paths in $N$ back to $M$ without losing convergence. The local-isometry property gives the path-lifting machinery, and completeness of $M$ ensures the lifted endpoints converge in $M$. This theorem and the previous one ([Local Isometry from Complete Manifold is a Covering Map](/theorems/2735)) form a pair: the previous theorem assumes surjectivity and lifts paths; the present theorem produces surjectivity from completeness of the domain plus connectedness of the codomain, and chains the two results. [/guided] [/step]