Brouwer fixed-point theorem for the closed unit ball in $\mathbb{R}^n$

Brouwer's fixed-point theorem for the closed unit ball. Let $n \ge 0$ and let

be the closed unit ball of Euclidean $n$-space. If $f : \overline{B}^n \to \overline{B}^n$ is continuous, then $f$ has a fixed point:

This is the topological core of Brouwer's theorem (Brouwer, 1911). The general form for an arbitrary nonempty compact convex subset $K$ of a finite-dimensional real normed space (AGT.brouwer_fixed_point, the Brouwer milestone of the mission Algorithmic Game Theory I) reduces to this special case: after identifying the ambient space with $\mathbb{R}^n$, the nearest-point projection $P : \mathbb{R}^n \to K$ is a nonexpansive retraction, so a fixed point of the rescaled map $y \mapsto R^{-1} f(P(Ry))$ on $\overline{B}^n$, where $K \subseteq \overline{B}(0,R)$, is a fixed point of $f$ on $K$. Conversely the ball is itself compact and convex, so the two statements are equivalent; this one isolates the part that needs a genuinely topological or combinatorial argument (Sperner's lemma, the no-retraction theorem via homology or Milnor's analytic argument, the Hex theorem, …), none of which is presently in Mathlib.

A note on the hypotheses. Continuity is only required on the ball and the values of $f$ outside the ball are irrelevant. The case $n = 0$ is included: $\mathbb{R}^0$ is a single point, the ball is that point, and it is trivially fixed. No nonemptiness hypothesis is needed because the closed unit ball is never empty.

Formalization Note. The ambient space is EuclideanSpace ℝ (Fin n), i.e. $\mathbb{R}^n$ with the $\ell^2$ norm, and the ball is Metric.closedBall 0 1. The map is given as a total function $f : \mathbb{R}^n \to \mathbb{R}^n$ together with ContinuousOn f (closedBall 0 1) and Set.MapsTo f (closedBall 0 1) (closedBall 0 1), matching the conventions of the parent statement AGT.brouwer_fixed_point.