Complete local isometry is a covering (source code)

= Complete local isometry is a covering

A <local isometry> from a nonempty complete <Riemannian manifold> to a connected Riemannian manifold is a surjective <covering map>. Lift radial <geodesics> in a normal ball using completeness; the <exponential map> at each inverse-image centre maps a tangent ball diffeomorphically onto a sheet. Uniqueness of the geodesic initial-value problem makes these sheets disjoint and exhaustive. Surjectivity follows by lifting piecewise geodesic paths. Conversely a Riemannian covering of a complete target is complete, by lifting complete target geodesics and using the <Hopf-Rinow theorem>. If the target is disconnected, the first assertion gives a covering only of the union of components met by the map.