CAT(0) space

A CAT(0) space is a geodesic metric space whose geodesic triangles are no thicker than their Euclidean comparison triangles.

A Hadamard space is a complete CAT(0) space. Equivalently, every pair has a midpoint $m$ satisfying the midpoint inequality $d(z,m{)}^2\le \frac{1}{2}d(z,x{)}^2+\frac{1}{2}d(z,y{)}^2-\frac{1}{4}d(x,y{)}^2$ for every $z$. This inequality makes the midpoint unique. Iterating midpoints and using completeness constructs the unique geodesic joining the pair. The squared-distance inequality extends to every point of that geodesic by dyadic approximation and implies Euclidean triangle comparison and geodesic convexity of closed balls.

For the constant-speed geodesic $\gamma$ from $x$ to $y$ in a Hadamard space, the displayed inequality follows by repeatedly applying the midpoint inequality and passing from dyadic parameters to all $t\in [0,1]$. Applying it on two sides of a triangle gives $d(x_s,y_t{)}^2\le s^2{A}^2+t^2{B}^2-st(A^2+B^2-C^2)$, where $A=d(a,x)$, $B=d(a,y)$ and $C=d(x,y)$. The right side is the squared comparison distance by the Euclidean cosine rule.