- If is geodesically complete, then given any two points there is a minimizing geodesic joining and .
- For any point , the exponential map at is surjective from to , and any length-minimizing curve from to for some , occurs as the image of a straight line from the origin, under the exponential map.
- Given , there exists , such that the exponential map takes the unit sphere of radius about to the set of points on the manifold at distance from , with the minimal geodesics from being exponentials of the radial paths.
The upshot of this is: given , there is an such that the set of points at distance from is a compact set, and such that there is a unique minimizing geodesic from to each of them
- Any geodesic can be extended indefinitely (and uniquely) in both directions (this follows from the assumption that our manifold is geodesically complete)
The proof beyond these two facts is purely geometric (that is, it only uses standard properties of metrics and continuous maps).