It seems fairly well-known that the KKM lemma of Knaster-Kuratowski-Mazurkiewicz implies Sperner's lemma (definitions below). However, I only know of indirect proofs, for instance that KKM can be used to prove Brouwer's fixed point theorem, and that the latter can be used to prove Sperner's lemma.
Question: Can Sperner's lemma be proved directly from the KKM lemma, without "intermediate stops" at for instance Brouwer, by suitably defining the sets $C_i$ in the KKM lemma below so that points in their intersection must lie in a completely labeled simplex?
What I tried: I searched the net without success. I thought it might work to define $C_i$ as the set of points in simplices with label $i$, but run into problems: if a point lies in the intersection of the $C_i$, it lies in a simplex with label $i$ for each $i$, but these simplices may be different for different $i$ and not necessarily, as desired, a single simplex with all labels.
Definitions: fix $n$ and let $\Delta = \{x \in \mathbb{R}^n: x_1, \ldots, x_n \geq 0, \sum_i x_i = 1\}$ denote the simplex. For each nonempty $J \subseteq \{1, \ldots, n\}$, let $\Delta_J = \{x \in \Delta: x_j = 0 \text{ for all } j \notin J\}$.
KKM lemma: If $C_1, \ldots, C_n$ are closed subsets of $\Delta$ such that $\Delta_J \subseteq \cup_{j \in J} C_j$ for each nonempty $J \subseteq \{1, \ldots, n\}$, then $\cap_{i=1}^n C_i \neq \emptyset$.
For Sperner's lemma, a simplicial subdivision of $\Delta$ is a finite collection of smaller closed simplices of the same dimension whose union is $\Delta$; the intersection of any two such smaller simplices must be empty or a face of both.
A Sperner labeling assigns a label $1, \ldots, n$ to each vertex of the subsimplices in this subdivision in such a way that $x_i = 0$ implies that its label is not $i$.
Sperner's lemma: Consider a simplicial subdivision of $\Delta$ and a Sperner labeling; this subdivision contains a simplex whose vertices have all labels $1, \ldots, n$.
I was surprised to find that this was not well-known. It took me a while, but in the end I could prove the result myself. The text below is taken almost verbatim from my note "An elementary direct proof that the Knaster-Kuratowski-Mazurkiewicz lemma implies Sperner's lemma", to appear in Economics Letters; see here or the preprint on Arxiv here.
The main idea is to use the fact that the vertices of simplices are affinely independent: each element of a simplex has a unique representation as a convex combination of its vertices.
Step 1: Define $C_i$
Fix label $i \in \{1, \ldots, n\}$. For each simplex $S = \text{conv} \{a_1, \ldots, a_n\}$ in the subdivision, define the possibly empty subset $T_S \subseteq S$ of convex combinations $\sum_j \lambda_j a_j$ giving weight $\lambda_j \geq 1/n$ to at least one vertex $a_j$ with label $i$. Let $C_i$ be the union of all these $T_S$. As the union of finitely many closed sets, $C_i$ is closed.
Step 2: Verify the KKM condition
Let $J \subseteq \{1, \ldots, n\}$ be nonempty. To show: $\Delta_J \subseteq \bigcup_{j \in J} C_j$. So let $x \in \Delta_J$. This $x$ is a convex combination $x = \sum_i \lambda_i a_i$ of vertices of a simplex $S = \text{conv} \{a_1, \ldots, a_n\}$ of the subdivision. At least one vertex $a_i$ has weight $\lambda_i \geq 1/n$. Since $x \in \Delta_J$, only coordinates of $x$ and hence of $a_i$ that lie in $J$ can be positive. By definition of the labeling, $\ell(a_i) \in J$. So $x \in C_{\ell(a_i)} \subseteq \bigcup_{j \in J} C_j$.
Step 3: Find a completely labeled simplex
By KKM, there is an $x^* \in \bigcap_i C_i$. By definition of $C_i$: for each label $i$, some simplex $S_i$ in the subdivision has $x^*$ as a convex combination of its vertices with a weight of at least $1/n$ on a vertex $v_i$ with label $i$. $S_1$ is completely labeled. Its vertex $v_1$ has label 1. For labels $p \neq 1$, note that $x^* \in S_1 \cap S_p$. This intersection is a face of $S_1$ and $S_p$. But then $v_p$ with label $p$ is one of the vertices (of $S_1$ and $S_p$) spanning this face: if not, $x^*$ would also be a convex combination of vertices of $S_p$ other than $v_p$, contradicting its unique representation in $S_p$.