Theorem 1.9: Brouwer fixed point theorem for $D^2$

Proved

Hatcher.brouwer_fixed_point_disk

by korbonits · Sep 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologycovering-spacesfundamental-grouphatcher

Let $D^2=\{x\in\mathbb{R}^2:\ |x|\le 1\}$ be the closed unit disk. Theorem 1.9. Every continuous map $h:D^2\to D^2$ has a fixed point, that is, a point $x\in D^2$ with

h(x)=x .

Hatcher proves it from Theorem 1.7: a fixed-point-free $h$ would yield a retraction $r:D^2\to S^1$ (send $x$ to the point where the ray from $h(x)$ through $x$ leaves the disk), and a retraction onto $S^1$ would make every loop in $S^1$ null-homotopic, contradicting $\pi_1(S^1)\neq 0$ .

Formalization Note $D^2$ is Metric.closedBall (0 : EuclideanSpace ℝ (Fin 2)) 1, the closed unit ball of the Euclidean plane, with the subspace topology; $h$ is a continuous map from this subspace to itself.

Preamble

import Definitions.Def_Hatcher_Circle
import Mathlib

open unitInterval Hatcher

Formal statement

namespace Hatcher
theorem brouwer_fixed_point_disk
    (h : C(Metric.closedBall (0 : EuclideanSpace ℝ (Fin 2)) 1,
          Metric.closedBall (0 : EuclideanSpace ℝ (Fin 2)) 1)) :
    ∃ x, h x = x := by sorry
end Hatcher

Source

A. Hatcher, Algebraic Topology, Cambridge University Press 2002, https://pi.math.cornell.edu/~hatcher/AT/AT.pdf, Section 1.1, p. 31, Theorem 1.9 (D^n denotes the closed unit disk in ℝ^n, all vectors of length ≤ 1)

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

Declaration Hatcher.brouwer_fixed_point_disk.

Let $E = \mathbb{R}^2$ be the real Euclidean plane realized as the type of functions $\{0,1\} \to \mathbb{R}$ (indexed by the two-element type), carrying the $\ell^2$ (Euclidean) norm

\|x\| = \sqrt{x_0^2 + x_1^2}, \qquad \operatorname{dist}(x,y) = \sqrt{(x_0-y_0)^2 + (x_1-y_1)^2}.

Let $D \subseteq E$ denote the closed ball of radius $1$ about the origin $0 = (0,0)$ with respect to this metric, i.e.

D = \{\, y \in E \;:\; \operatorname{dist}(y, 0) \le 1 \,\} = \{\, y \in E : \|y\| \le 1 \,\},

viewed as a topological space in its own right with the subspace topology inherited from $E$ (the topology induced by the inclusion $D \hookrightarrow E$ ; since the norm on $\mathbb{R}^2$ is the Euclidean one, this is the usual topology on the closed unit disk).

The statement quantifies over a single explicit hypothesis-object $h$ : a continuous map $h : D \to D$ , that is, a pair consisting of a function from $D$ to $D$ together with a proof that this function is continuous for the subspace topology on both source and target. No further hypotheses are imposed on $h$ (in particular nothing beyond continuity: no smoothness, injectivity, surjectivity, or boundary behaviour is assumed).

The conclusion asserts:

\exists\, x \in D,\quad h(x) = x .

Here $x$ ranges over points of $D$ (elements of the closed unit disk, i.e. points $x \in \mathbb{R}^2$ with $\|x\| \le 1$ ), and the equality $h(x) = x$ is equality of points of $D$ , which amounts to equality of the underlying points of $\mathbb{R}^2$ . The existential is plain existence ( $\exists$ ), not unique existence; nothing is claimed about the number or location of fixed points, and $x$ is permitted to lie anywhere in $D$ , including on the boundary circle $\|x\| = 1$ or at the origin.

Degenerate/edge remarks about what the quantifiers include: $D$ is nonempty (it contains $0$ ), so the existential is not trivially unsatisfiable on emptiness grounds; the radius $1$ and centre $0$ are fixed constants, so the statement is about this one specific closed disk and is not parametrized over other radii, centres, or dimensions. The declaration uses no custom definitions from the accompanying bundle; every notion it mentions (Euclidean plane with $\ell^2$ norm, closed metric ball, continuous map between subspaces) is standard Mathlib.

Human review

Endorsed by Shuze Chen · Sep 5, 2026
Endorsed by korbonits · Sep 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 1.9: Brouwer fixed point theorem for D2D^2D2

Theorem 1.9: Brouwer fixed point theorem for $D^2$