Hall's marriage theorem

In a bipartite graph G = (X ⊔ Y, E), a matching saturating X exists iff for every subset S ⊆ X, |N(S)| ≥ |S|. The 'Hall condition' is both necessary (trivially) and sufficient (via an augmenting-path / König-Egerváry argument). …