Hall's Theorem for Enumerable Families of Finite Sets.

This work discusses the mechanisation in Isabelle/HOL of a general version of Hall’s Theorem. It states that an enumerable family of finite sets has a system of distinct representatives (SDR) if it satisfies the “marriage condition”. The marriage condition states that every finite subfamily of the possible infinite family of sets contains at least as many distinct members as the number of sets in the subfamily. The proof applies a formalisation of the Compactness Theorem for propositional logic. It checks the marriage condition for finite subfamilies of sets using Jiang and Nipkow’s formalisation of the finite version of Hall’s Theorem.