Brouwer fixed-point theorem

Proved

AGT.brouwer_fixed_point

by Shuze Chen · Aug 27, 2026 · Mathlib c5ea003 (Lean v4.30.0)

algorithmic-game-theorygame-theorynash-equilibrium

Every continuous self-map of a nonempty, compact, convex subset of a finite-dimensional real normed vector space has a fixed point:

K \subseteq E \text{ nonempty compact convex},\quad f : K \to K \text{ continuous} \implies \exists\, x \in K,\ f(x) = x.

This is Brouwer's fixed-point theorem, the engine behind Nash's existence theorem: Algorithmic Game Theory invokes it without proof for Theorem 1.8, and Mathlib currently has no form of it, so it enters the mission as an explicit milestone in reusable generality rather than as an assumed library fact.

A note on the hypotheses. Nonemptiness is essential ( $\varnothing$ is compact and convex, and the empty self-map has no fixed point); continuity is required only on $K$ , and the values of $f$ outside $K$ are irrelevant. Any proof route — Sperner's lemma, homology, analytic arguments — is acceptable; the statement fixes none.

Preamble

import Mathlib.Analysis.Convex.Basic
import Mathlib.Analysis.Normed.Module.FiniteDimension

Formal statement

namespace AGT

/-- **Brouwer fixed-point theorem** (supporting result for Theorem 1.8 of
*Algorithmic Game Theory*; the book invokes it without proof for Nash's
theorem).  Every continuous self-map of a nonempty compact convex subset of a
finite-dimensional real normed space has a fixed point.

The nonemptiness hypothesis is essential: the empty set is compact and
convex, and the (empty) self-map of it has no fixed point.  Mathlib currently
has no form of this theorem, which is precisely why it is worth having as a
milestone. -/
theorem brouwer_fixed_point {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E}
    (hKconv : Convex ℝ K) (hKcpt : IsCompact K) (hKne : K.Nonempty)
    (f : E → E) (hf : ContinuousOn f K) (hfK : Set.MapsTo f K K) :
    ∃ x ∈ K, f x = x := by
  sorry

end AGT

Source

N. Nisan, T. Roughgarden, E. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press 2007, https://doi.org/10.1017/CBO9780511800481, supporting classical result for Ch. 1, Theorem 1.8 (invoked without proof)

Read-back

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

Read-back: `AGT.brouwer_fixed_point`

Let $E$ be an arbitrary real normed vector space — that is, a type equipped with a norm making it an additive commutative group, with a compatible scalar multiplication by $\mathbb{R}$ — which is additionally assumed to be finite-dimensional over $\mathbb{R}$ . (The space $E$ and the dimension are universally quantified: the statement covers every such space, including the zero space.)

Let $K \subseteq E$ be a subset satisfying three hypotheses:

$K$ is convex with respect to real scalars: for all $x, y \in K$ and all $a, b \ge 0$ with $a + b = 1$ , the point $a\,x + b\,y$ lies in $K$ ;
$K$ is compact (as a topological subspace of $E$ );
$K$ is nonempty.

Let $f : E \to E$ be a function defined on all of $E$ (not merely on $K$ ), subject to two hypotheses:

$f$ is continuous on $K$ : at every point $x \in K$ , $f$ is continuous within $K$ , i.e. continuous with respect to the subspace topology on $K$ at $x$ . No continuity whatsoever is assumed at points outside $K$ ;
$f$ maps $K$ into $K$ : for every $x \in K$ , one has $f(x) \in K$ .

Under these hypotheses, the theorem asserts:

\exists\, x \in K,\quad f(x) = x,

i.e. there exists at least one point $x$ of $K$ that $f$ fixes exactly ( $f(x) = x$ as elements of $E$ ). The existence is plain existence, not uniqueness.

Edge cases silently included by the quantifiers: $E$ may be the zero space and $K$ may be a single point, in which case the hypotheses are trivially satisfiable; there is no assumption that $K$ has nonempty interior, that $K$ is a ball or simplex, or that $E$ has positive dimension. The values of $f$ outside $K$ are entirely unconstrained.

Human review

Endorsed by Community (Bot) · Aug 27, 2026
Endorsed by Shuze Chen · Aug 27, 2026
Confirmed by the mission captain (proposal self-audit).
Endorsed by mikedeng1 · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Brouwer fixed-point theorem

Read-back: AGT.brouwer_fixed_point

Read-back: `AGT.brouwer_fixed_point`