# Hall's Marriage Theorem #

Given a list of finite subsets $X_1, X_2, \dots, X_n$ of some given set $S$, P. Hall in [Hal35] gave a necessary and sufficient condition for there to be a list of distinct elements $x_1, x_2, \dots, x_n$ with $x_i\in X_i$ for each $i$: it is when for each $k$, the union of every $k$ of these subsets has at least $k$ elements.

Rather than a list of finite subsets, one may consider indexed families t : ι → Finset α of finite subsets with ι a Fintype, and then the list of distinct representatives is given by an injective function f : ι → α such that ∀ i, f i ∈ t i, called a matching. This version is formalized as Finset.all_card_le_biUnion_card_iff_exists_injective' in a separate module.

The theorem can be generalized to remove the constraint that ι be a Fintype. As observed in [Hal66], one may use the constrained version of the theorem in a compactness argument to remove this constraint. The formulation of compactness we use is that inverse limits of nonempty finite sets are nonempty (nonempty_sections_of_finite_inverse_system), which uses the Tychonoff theorem. The core of this module is constructing the inverse system: for every finite subset ι' of ι, we can consider the matchings on the restriction of the indexed family t to ι'.

## Main statements #

• Finset.all_card_le_biUnion_card_iff_exists_injective is in terms of t : ι → Finset α.
• Fintype.all_card_le_rel_image_card_iff_exists_injective is in terms of a relation r : α → β → Prop such that Rel.image r {a} is a finite set for all a : α.
• Fintype.all_card_le_filter_rel_iff_exists_injective is in terms of a relation r : α → β → Prop on finite types, with the Hall condition given in terms of finset.univ.filter.

## TODO #

• The statement of the theorem in terms of bipartite graphs is in preparation.

## Tags #

Hall's Marriage Theorem, indexed families

def hallMatchingsOn {ι : Type u} {α : Type v} (t : ι) (ι' : ) :
Set ({ x : ι // x ι' }α)

The set of matchings for t when restricted to a Finset of ι.

Equations
• = {f : { x : ι // x ι' }α | ∀ (x : { x : ι // x ι' }), f x t x}
Instances For
def hallMatchingsOn.restrict {ι : Type u} {α : Type v} (t : ι) {ι' : } {ι'' : } (h : ι' ι'') (f : (hallMatchingsOn t ι'')) :
()

Given a matching on a finset, construct the restriction of that matching to a subset.

Equations
• = fun (i : { x : ι // x ι' }) => f i, ,
Instances For
theorem hallMatchingsOn.nonempty {ι : Type u} {α : Type v} [] (t : ι) (h : ∀ (s : ), s.card (s.biUnion t).card) (ι' : ) :
Nonempty ()

When the Hall condition is satisfied, the set of matchings on a finite set is nonempty. This is where Finset.all_card_le_biUnion_card_iff_existsInjective' comes into the argument.

def hallMatchingsFunctor {ι : Type u} {α : Type v} (t : ι) :

This is the hallMatchingsOn sets assembled into a directed system.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance hallMatchingsOn.finite {ι : Type u} {α : Type v} (t : ι) (ι' : ) :
Finite ()
Equations
• =
theorem Finset.all_card_le_biUnion_card_iff_exists_injective {ι : Type u} {α : Type v} [] (t : ι) :
(∀ (s : ), s.card (s.biUnion t).card) ∃ (f : ια), ∀ (x : ι), f x t x

This is the version of Hall's Marriage Theorem in terms of indexed families of finite sets t : ι → Finset α. It states that there is a set of distinct representatives if and only if every union of k of the sets has at least k elements.

Recall that s.biUnion t is the union of all the sets t i for i ∈ s.

This theorem is bootstrapped from Finset.all_card_le_biUnion_card_iff_exists_injective', which has the additional constraint that ι is a Fintype.

instance instFintypeElemImageToSetOfDecidableEqOfSingletonSet {α : Type u} {β : Type v} [] (r : αβProp) [(a : α) → Fintype (Rel.image r {a})] (A : ) :
Fintype (Rel.image r A)

Given a relation such that the image of every singleton set is finite, then the image of every finite set is finite.

Equations
theorem Fintype.all_card_le_rel_image_card_iff_exists_injective {α : Type u} {β : Type v} [] (r : αβProp) [(a : α) → Fintype (Rel.image r {a})] :
(∀ (A : ), A.card Fintype.card (Rel.image r A)) ∃ (f : αβ), ∀ (x : α), r x (f x)

This is a version of Hall's Marriage Theorem in terms of a relation between types α and β such that α is finite and the image of each x : α is finite (it suffices for β to be finite; see Fintype.all_card_le_filter_rel_iff_exists_injective). There is a transversal of the relation (an injective function α → β whose graph is a subrelation of the relation) iff every subset of k terms of α is related to at least k terms of β.

Note: if [Fintype β], then there exist instances for [∀ (a : α), Fintype (Rel.image r {a})].

theorem Fintype.all_card_le_filter_rel_iff_exists_injective {α : Type u} {β : Type v} [] (r : αβProp) [(a : α) → DecidablePred (r a)] :
(∀ (A : ), A.card (Finset.filter (fun (b : β) => aA, r a b) Finset.univ).card) ∃ (f : αβ), ∀ (x : α), r x (f x)

This is a version of Hall's Marriage Theorem in terms of a relation to a finite type. There is a transversal of the relation (an injective function α → β whose graph is a subrelation of the relation) iff every subset of k terms of α is related to at least k terms of β.

It is like Fintype.all_card_le_rel_image_card_iff_exists_injective but uses Finset.filter rather than Rel.image.