# 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

The set of matchings for `t`

when restricted to a `Finset`

of `ι`

.

## Equations

- hallMatchingsOn t ι' = {f : { x : ι // x ∈ ι' } → α | Function.Injective f ∧ ∀ (x : { x : ι // x ∈ ι' }), f x ∈ t ↑x}

## Instances For

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

## Equations

- hallMatchingsOn.restrict t h f = ⟨fun (i : { x : ι // x ∈ ι' }) => ↑f ⟨↑i, ⋯⟩, ⋯⟩

## Instances For

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.

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

## Equations

- ⋯ = ⋯

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`

.

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

## Equations

- instFintypeElemImageToSetOfDecidableEqOfSingletonSet r A = let_fun h := ⋯; ⋯.mpr (FinsetCoe.fintype (A.biUnion fun (a : α) => (Rel.image r {a}).toFinset))

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})]`

.

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`

.