Facets of a full grid simplex are its vertex deletions

Proved

Plasticity.Ext.Brouwer.facets

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

In a Sperner cube of dimension $n=n_1+1$ , let $J$ be a grid $n$ -simplex and $I$ a list of $n_1+1$ grid points. Then $I$ is a face of $J$ if and only if $I$ is obtained from $J$ by deleting one vertex (keeping the order of the others).

It is the first counting step of Kuhn's cubical Sperner lemma.

Preamble

import Definitions.Def_Plasticity_CubicalSperner

Formal statement

namespace Plasticity.Ext.Brouwer
theorem facets (SC : CubicalSperner.SpernerCube) {n1 : ℕ} (hn1 : n1 + 1 = SC.n)
    (I : Fin (n1 + 1) → SC.G) (J : Fin (SC.n + 1) → SC.G) (hJ : CubicalSperner.simplex SC SC.n J) :
    CubicalSperner.is_face SC I J ↔ ∃ i, I = @CubicalSperner.delete_vertex SC n1 hn1 i J := by sorry
end Plasticity.Ext.Brouwer

Source

H. W. Kuhn, IBM J. Res. Dev. 4 (1960); ported from harfe/fixed-point-theorems-lean4 (MIT)

View graph