Brouwer Fixed-Point Theorem

Statement

Let $D^n = \{x \in \mathbb{R}^n : \|x\| \le 1\}$ be the closed unit ball. Every continuous map $f : D^n \to D^n$ has a fixed point:

The $n=1$ case is immediate from the Intermediate Value Theorem; the general case requires algebraic topology (homology or degree theory).

Visualization

In 1D, the theorem says every continuous $f : [0,1] \to [0,1]$ crosses the diagonal.

1 │                  ╱ y = x (diagonal)
  │            ╱
  │       ╱  ╳────── f(x) crosses y=x here → fixed point!
  │    ╱  ╱
  │ ╱  ╱
0 └────────────────── 1
  0                  1

If f(0) ≥ 0 and f(1) ≤ 1, let g(x) = f(x) − x.
  g(0) = f(0) − 0 ≥ 0
  g(1) = f(1) − 1 ≤ 0
IVT → ∃ x* with g(x*) = 0, i.e. f(x*) = x*.

Intuitively: crumple a piece of paper and lay it on a copy of itself — at least one point lands exactly on its original position.

Proof Sketch

One dimension. Define $g(x) = f(x) - x$. Then $g(0) = f(0) \ge 0$ and $g(1) = f(1) - 1 \le 0$. Since $g$ is continuous, the Intermediate Value Theorem yields $x^* \in [0,1]$ with $g(x^*) = 0$, i.e. $f(x^*) = x^*$.

General $n$. Suppose for contradiction $f$ has no fixed point. Define a retraction $r : D^n \to S^{n-1}$ by drawing the ray from $f(x)$ through $x$ and letting $r(x)$ be where it meets $S^{n-1}$. This $r$ would be a continuous retraction of $D^n$ onto $S^{n-1}$, contradicting the fact that $S^{n-1}$ is not a retract of $D^n$ (witnessed by homology: $H_{n-1}(S^{n-1}) \cong \mathbb{Z}$ but $H_{n-1}(D^n) = 0$). Mathlib contains the full $n$-dimensional proof in Mathlib.Topology.Homotopy.Brouwer.

Connections

• Heine–Borel TheoremHeine–Borel Theorem$$K \subseteq \mathbb{R}^n \;\text{compact} \iff K \;\text{closed and bounded}$$In ℝⁿ, a subset is compact if and only if it is closed and boundedRead more → — the closed unit ball is compact (closed and bounded); compactness is essential for most existence proofs.
• Bolzano–Weierstrass TheoremBolzano–Weierstrass Theorem$$\text{bounded } (x_n) \subseteq \mathbb{R}^n \implies \exists\, \text{convergent subsequence}$$Every bounded sequence in ℝⁿ has a convergent subsequenceRead more → — the 1D proof uses the Intermediate Value Theorem, closely related to the nested interval argument behind Bolzano–Weierstrass.
• Tychonoff's TheoremTychonoff's Theorem$$\prod_{i \in I} X_i \text{ compact} \iff \forall i,\; X_i \text{ compact}$$An arbitrary product of compact spaces is compact in the product topologyRead more → — in infinite dimensions (e.g. Hilbert space), Tychonoff's theorem helps recover a version via the Schauder fixed-point theorem.
• Urysohn's LemmaUrysohn's Lemma$$\exists\, f : X \to [0,1],\quad f|_s = 0,\; f|_t = 1$$In a normal space, disjoint closed sets can be separated by a continuous functionRead more → — separation of points is used in the homological proof to construct test functions distinguishing boundary from interior.
• Hausdorff DistanceHausdorff Distance$$d_H(A, B) = \max\left(\sup_{a \in A} d(a, B),\ \sup_{b \in B} d(b, A)\right)$$A metric on non-empty compact sets, foundation for the IFS attractor theoremRead more → — iterated approximation schemes for fixed points converge in the Hausdorff metric on compact sets.
• Iterated Function SystemsIterated Function Systems$$A = \bigcup_{i=1}^{N} f_i(A)$$Constructing fractals via contractive affine transformationsRead more → — IFS attractors are Banach fixed points in the Hausdorff metric space; Brouwer's theorem gives a topological (not metric) companion existence result.
• Banach Fixed Point TheoremBanach Fixed Point Theorem$$T : X \to X\text{ contraction} \Rightarrow \exists!\, x^* = T(x^*)$$Every contraction on a complete metric space has a unique fixed point, reached by iterating the mapRead more → — the metric complement: Banach requires a contraction on a complete metric space and gives a unique fixed point with explicit rate-of-convergence; Brouwer requires only continuity on a compact convex set but gives no uniqueness or constructive approximation.

Lean4 Proof

The 1D fixed-point theorem follows directly from Mathlib's intermediate_value_Icc.