Proof. [02CJ]
Original official author HTML, exact retained edition. Historical TeX conversion verdicts remain unchanged. Cited-edition alignment and mathematical self-containment are not assessed.
Complete original source context · Original author HTML
Proof.
Fix any point in , choose a convex embedded ball in . We claim for all . For otherwise there is a such that for but is non-empty. Choose a point in this intersection. Let be the radial geodesic connecting and , and let . Then , and . Consider the pointed sequence . By assumption we know as tends to infinity by passing to a subsequence this converges to a tangent cone . Then the rescaled balls converge to a ball in and . But is isometric to a ball in so have uniformly bounded geometry and thus converges to a flat ball . Moreover by Lemma 5.3 the distance between any two points in is realized by the length of a geodesic within . Clearly this can not happen on .
By the claim the isometric action is well defined on for all . Then we can extend the action to an isometric action on : given we pick a Cauchy sequence converging to ; for any , is also a Cauchy sequence in , so there is a unique limit . We define . Clearly is distance preserving. Moreover preserves both and . ∎