Cubical Sperner lemma: a fully labelled small grid simplex exists

Proved

Plasticity.Ext.Brouwer.sperner

by scanstone · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

Let $L$ label the grid $\{0,\dots,p\}^n$ with numbers $0,\dots,n$ such that a point whose $k$ -th coordinate is $0$ does not carry label $k$ , and a point whose $k$ -th coordinate is $p$ carries a label at most $k$ . Then there are $n+1$ grid points $I_0,\dots,I_n$ , any two within $1$ of each other in every coordinate, that carry all the labels $0,\dots,n$ .

Applied to finer and finer grids, it gives Brouwer's fixed-point theorem for the cube.

Preamble

import Mathlib.Data.Fin.Basic

Formal statement

namespace Plasticity.Ext.Brouwer
theorem sperner (n p : ℕ) (L : (Fin n → Fin (p + 1)) → ℕ)
    (hL : ∀ v, L v ≤ n ∧ ∀ k : Fin n, (v k = 0 → L v ≠ k.1) ∧ (v k = Fin.last p → L v ≤ k.1)) :
    ∃ I : Fin (n + 1) → (Fin n → Fin (p + 1)),
      (∀ a b k, (I a k : ℕ) ≤ (I b k : ℕ) + 1) ∧ ∀ c ≤ n, ∃ a, L (I a) = c := by sorry
end Plasticity.Ext.Brouwer

Source

H. W. Kuhn, Some combinatorial lemmas in topology, IBM J. Res. Dev. 4 (1960), 518–524; ported from harfe/fixed-point-theorems-lean4 (MIT)

View graph