Hopf-Rinow lemma (source code)

= Hopf-Rinow lemma
{c}

If the <Riemannian exponential map> at one point $p$ of a connected finite-dimensional <Riemannian manifold> is defined on all of $T_pM$, every point can be joined to $p$ by a <minimizing geodesic>. The <distance splitting through a small geodesic sphere> selects a radial direction attaining $d(p,q)=r+d(\gamma(r),q)$. If this equality stopped before the target, repeat the splitting at its last point. A broken minimizing path cannot have a corner, so the new segment continues the same <geodesic>, contradicting maximality. This is the minimizing-geodesic lemma used in the <radial continuation proof of Hopf-Rinow>.

// Target: riemannian-geometry.bigb