Theorem 6.2 — Hall's marriage theorem

For every finite type $V$ equipped with a finite enumeration, every simple undirected loopless graph $G$ on $V$ equipped with finite enumerations of all its neighbor sets, and every pair of sets $L,R \subseteq V$, assume that $L$ and $R$ are disjoint, every edge of $G$ has one endpoint in $L$ and the other in $R$, and $L \cup R=V$. Then the following two assertions are equivalent: there exists a subgraph $M$ of $G$ such that every vertex of $M$ has exactly one neighbor in $M$ and $L$ is contained in the vertex set of $M$; and, for every set $S \subseteq L$, $|S| \leq |N_G(S)|$, where $N_G(S)=\{w \in V : \text{there is }v \in S\text{ adjacent to }w\text{ in }G\}$ is the union of the neighbor sets of the vertices of $S$. A subgraph chooses a vertex set and some of the edges of $G$, with both endpoints of every chosen edge in that vertex set. The existence assertion does not require uniqueness of $M$ or require $M$ to contain every vertex of $R$. The neighbor union counts each vertex once, even when it is adjacent to several vertices of $S$, and the assumptions imply that this union lies in $R$. Both displayed cardinalities are natural-number set cardinalities: they are ordinary finite counts here because $V$ is finite; the general convention that an infinite set has natural-number cardinality zero never applies under these hypotheses. The universal condition includes $S=\varnothing$, when the inequality is $0 \leq 0$. Empty vertex types and empty parts are allowed. If $L=\varnothing$, both assertions hold, with the empty subgraph as a witness. If $R=\varnothing$ and $L$ is nonempty, both assertions are false, since the graph has no edges and any singleton subset of $L$ violates the inequality. No infinite vertex type is covered by this theorem.