Hall's Marriage Theorem for finite index types #
This module proves the basic form of Hall's theorem.
In contrast to the theorem described in Combinatorics.Hall.Basic
, this
version requires that the indexed family t : ι → Finset α
have ι
be finite.
The Combinatorics.Hall.Basic
module applies a compactness argument to this version
to remove the Finite
constraint on ι
.
The modules are split like this since the generalized statement depends on the topology and category theory libraries, but the finite case in this module has few dependencies.
A description of this formalization is in [GMM].
Main statements #
Finset.all_card_le_biUnion_card_iff_existsInjective'
is Hall's theorem with a finite index set. This is elsewhere generalized toFinset.all_card_le_biUnion_card_iff_existsInjective
.
Tags #
Hall's Marriage Theorem, indexed families
First case of the inductive step: assuming that
∀ (s : Finset ι), s.Nonempty → s ≠ univ → s.card < (s.biUnion t).card
and that the statement of Hall's Marriage Theorem is true for all
ι'
of cardinality ≤ n
, then it is true for ι
of cardinality n + 1
.
Second case of the inductive step: assuming that
∃ (s : Finset ι), s ≠ univ → s.card = (s.biUnion t).card
and that the statement of Hall's Marriage Theorem is true for all
ι'
of cardinality ≤ n
, then it is true for ι
of cardinality n + 1
.
Here we combine the two inductive steps into a full strong induction proof, completing the proof the harder direction of Hall's Marriage Theorem.
This is the version of Hall's Marriage Theorem in terms of indexed
families of finite sets t : ι → Finset α
with ι
finite.
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.
See Finset.all_card_le_biUnion_card_iff_exists_injective
for a version
where the Finite ι
constraint is removed.