No continuous retraction of the closed unit ball onto its boundary sphere

The no-retraction theorem. Let $n \ge 0$, let $\overline{B}^n = \{x \in \mathbb{R}^n : \|x\|_2 \le 1\}$ be the closed unit ball and $S^{n-1} = \{x : \|x\|_2 = 1\}$ its boundary sphere. There is no continuous retraction of the ball onto its boundary: no map $r : \overline{B}^n \to S^{n-1}$ that is continuous and satisfies

Equivalently, the identity map of $S^{n-1}$ does not extend to a continuous map $\overline{B}^n \to S^{n-1}$. This is the classical form in which Brouwer's fixed-point theorem is usually proved: in homological language it says that $S^{n-1}$ is not contractible via the ball ($H_{n-1}(S^{n-1}) \ne 0$ while $H_{n-1}(\overline{B}^n) = 0$); Milnor (1978) and Rogers (1980) give analytic proofs that avoid homology by smoothing $r$ and computing the volume of the image of $x \mapsto x + t\,(r(x) - x)$ as a polynomial in $t$. The theorem is equivalent to Brouwer's fixed-point theorem for the ball (AGT.brouwer_fixed_point_unitBall): a fixed-point-free continuous self-map $f$ of the ball yields the retraction sending $x$ to the point where the ray from $f(x)$ through $x$ leaves the ball, and conversely a retraction $r$ composed with the antipodal map is a fixed-point-free self-map.

A note on the hypotheses. For $n = 0$ the ball is a single point and the sphere is empty, so no map into the sphere exists at all and the statement holds vacuously; for $n = 1$ it is the intermediate value theorem. Continuity is only required on the ball; values of $r$ outside the ball are irrelevant.

Formalization Note. The ambient space is EuclideanSpace ℝ (Fin n); the ball is Metric.closedBall 0 1 and the sphere Metric.sphere 0 1. The retraction is given as a total function r : ℝⁿ → ℝⁿ with ContinuousOn r (closedBall 0 1), Set.MapsTo r (closedBall 0 1) (sphere 0 1), and the fixed-point condition on the sphere; the conclusion is False.