A local isometry here is a local diffeomorphism whose pullback metric is the source metric. Use the usual convention that a covering map is surjective. Assume the target is connected and the source is nonempty; this is the connected-manifold setting of the intended assertion. For a disconnected target the precise result is a covering of the union of target components met by the map. For example, inclusion is a local isometry from a complete manifold but is not a surjective covering of the whole target.
The correct Hopf-Rinow theorem says that on a connected finite-dimensional Riemannian manifold, completeness for the induced distance is equivalent to geodesic completeness, and to compactness of every closed bounded subset. These conditions imply that every two points are joined by a minimizing geodesic. The last property by itself does not imply completeness: an open Euclidean ball has minimizing segments between every pair but is incomplete.
A local isometry preserves the Levi-Civita connection, by uniqueness of the torsion-free metric connection on each local isometry chart. Hence it preserves affinely parametrized geodesics, and
whenever the source geodesic is defined. This is geodesic preservation by a local isometry.
Suppose is complete. Given , join to by a minimizing target geodesic using target completeness. The source geodesic whose initial velocity is its inverse image under exists for its full parameter interval by source completeness; its image is the target geodesic by uniqueness. Thus is onto.
Choose a normal ball with a diffeomorphism on . For every put . Source completeness defines these exponential maps throughout the tangent balls. The displayed exponential identity makes a diffeomorphism: injectivity follows from injectivity of the target exponential map, and differentiating the identity shows the source exponential has invertible derivative on the ball, so its image is open.
These sheets are disjoint. If lay in two, lift the reversed radial target geodesic from to , starting at . Its initial velocity is uniquely fixed by ; uniqueness of the source geodesic forces the two sheet centres to be equal. They exhaust : for any point over , lift that reversed radial geodesic using source completeness, obtaining a centre over , and then reverse it. Thus is evenly covered. This proves the complete local isometry is a covering assertion.
Conversely suppose is a covering. Given any initial tangent vector in , the corresponding target geodesic extends over all by target completeness. The path lifting theorem for coverings lifts it over every compact time interval, with uniqueness gluing the lifts to a curve on . In local covering charts the lift is a geodesic, because the charts are local isometries. It extends the source initial-value geodesic. Therefore is geodesically complete, and Hopf-Rinow yields metric completeness on each source component. In the stated connected-target setting,
Take the circular cylinder
Its first fundamental form is . The universal covering parametrization is therefore a local isometry from the Euclidean plane, after scaling the first coordinate. By geodesic preservation by a local isometry, every geodesic on the cylinder lifts to a straight line defined for all . Thus the cylinder is geodesically complete. It is noncompact because is unbounded, and it is not a plane because one of its principal curvatures is .