Dependencies

\(f\colon X \to X\) continuous and \(X\) compact metric space. Suppose that \(\forall \epsilon {\gt}0\), there exists \(x\in X\) such that \(d(f(x),x) {\lt} \epsilon \). Then \(f\) has a fixed point.

The baricenter of points \(p_1, \dots , p_k\) is \(B(p_1, \dots , p_k)= \frac{1}{k}\sum _{i=1}^k p_i\)

Let \(S\subseteq \mathbb {R}^n\) be a \(n\)-dimensional simplex with barycentric coordinates \(x_0,\ldots ,x_n\). The barycentric subdivison is a map form permutations of the \(n+1\) vertices of \(S\) to \(n\)-dimensional simplexes defined as follows

See end of https://github.com/leanprover-community/mathlib/blob/sperner-again/src/combinatorics/simplicial_complex/subdivision.lean

Let \(\Delta \) be a simplex. Given an ordered list of its vertices, and a function \(f:\Delta \to \Delta \), the induced color of a point \(x\in \Delta \) is \(i=\min \{ j ~ |~ f(x)_j {\lt} x_j\} \).

Let \(\hat S = B(v_0,v_1,\dots , v_k)\) be the barycenter of \(S\). We bound the distance of any vertex \(v_i\) of \(S\) to \(\hat S\). Given a simplex \(S\) of diameter \(D\), its barycentric subdivision has diameter at most \(\frac{n}{n+1}D\)

Let \(S\) be a \(k\)-dimensional simplex with vertices \(v_0, \dots , v_k\). The diameter of \(S\) \( Diam(S)= \max _{x,y\in S} |x-y|\) equals \(\max |v_i - v_j|\).

For all \(\epsilon {\gt}0\), there exists a subdivision of \(\Delta \) of diameter \({\lt}\epsilon \).

The coloring above is a Sperner coloring.

Given a simplicial complex \(S\), and a a coloring \(f\) on it, we say that \(f\) is a Sperner coloring of \(S\) if \(f(x) \neq i\) if \(x\) belongs to the \(i\)-th face (that with zero \(i\)-th coordinate).

For all \(\varepsilon {\gt}0\) exists \(\delta {\gt}0\), such that given a panchromatic simplex \(X\subseteq \Delta \) of a diameter \(\leq \delta \) then \(|f(x) - x| {\lt} \varepsilon ,\ \forall x \in X\).

A simplicial complex with a Sperner coloring on it, contains a panchromatic simplex.