Question: In the paper [Hall's theorem for hypergraphs (Aharoni and Haxell, 2000)](https://onlinelibrary.wiley.com/doi/abs/10.1002/1097-0118(200010)35:2%3C83::AID-JGT2%3E3.0.CO;2-V),
the authors prove a theorem on the existence of perfect matchings in bipartite hypergraphs, using Sperner's lemma. At the last page (6), they say that "we have here a topological proof of Hall's theorem" (for bipartite graphs). I thought it should be easy to write this proof explicitly, since a simple bipartite graph is just a bipartite hypergraph in which each hyperedge is of size 2. But there is a problem: during the proof, the authors assume that the sets of neighbors (i.e., the sets $N(x)$ for each vertex $x\in X$, where $X$ is one part of the hypergraph) are pairwise-disjoint. For a hypergraph, this assumption is without loss of generality, since we can add dummy vertices to edges, and this does not affect the theorem conditions or concludion. But in a graph, we cannot add vertices to edges.

So my question is: is there an explicitly-written proof of Hall's marriage theorem, using Sperner's lemma (or a similar topological theorem)?

Answer: 
Penny Haxell's 2011 paper [On Forming Committees](https://www.jstor.org/stable/10.4169/amer.math.monthly.118.09.777) in the American Mathematical Monthly explicitly uses Sperner's lemma to prove Hall's theorem for bipartite graphs (see theorem 4.1 and 4.2).
In addition to Carlo Beenakker's answer that gives Hall via Sperner directly, I think you can also get it by applying Hall's Theorem for Hypergraphs as follows. Let $G$ be a bipartite graph with partite sets $X, Y$, and write $V(X) = \{x\_1, \ldots, x\_n\}$. For each $i$, define a $1$-uniform hypergraph $H\_i$ with vertex set $N(x\_i)$ and edge set $\{ \{y\} : y \in N(x\_i) \}$.

Letting $\mathcal{A} = \{H\_1, \ldots, H\_n\}$, we see that $\mathcal{A}$ has a disjoint set of representatives if and only if $G$ has a matching that saturates $X$. Now the condition of Aharoni and Haxell's Theorem 1.1 applied to the family $\mathcal{A}$ is clearly equivalent to Hall's Condition on $G$. Since classical Hall's Theorem falls out of the hypergraph version so quickly, I think it's fair to think of the topological proof of the hypergraph version as also being a topological proof of Hall's theorem.