Lemma 8.7.3 — boundary characterization of the unique smallest enclosing ball

Let $B$ be the closed ball in $\mathbb{R}^d$ with center $s^*$ and radius $r\ge 0$, and let $S=\{s_1,\dots,s_k\}$ be points on the boundary of $B$, i.e. $\|s_j-s^*\|=r$ for all $j$. Then the following two statements are equivalent.

1. $B$ is the unique smallest enclosing ball of $S$: it contains $S$, every ball containing $S$ has radius at least $r$, and every ball containing $S$ with radius at most $r$ has center $s^*$.
2. For every $u\in\mathbb{R}^d$ there is an index $j\in\{1,\dots,k\}$ with

Condition 2 says that no hyperplane strictly separates $S$ from $s^*$. The lemma characterizes smallest enclosing balls by their boundary points and is the geometric half of the proof of Theorem 8.7.4.

Formalization Note The points are indexed by Fin k (0-based) and $S$ is their range; $u^T(s_j-s^*)$ is the Euclidean inner product. For $k=0$ both statements are false (a ball of negative radius, which is empty, encloses $S=\emptyset$; and no index exists), so no hypothesis $k\ge 1$ is needed.