Closest point on a geodesic line in a hyperbolic metric space (source code)

= Closest point on a geodesic line in a hyperbolic metric space

If $\gamma:\mathbb R\to X$ is an isometrically embedded geodesic line, then every $x\in X$ has a closest point on $\gamma$. The function $t\mapsto d(x,\gamma(t))$ is continuous and tends to infinity with $|t|$. Any two minimizing parameters differ by at most $4\delta$, and therefore by at most $6\delta$, in a $\delta$-hyperbolic metric space.