Hall's Marriage Theorem for finite index types #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This module proves the basic form of Hall's theorem.
In constrast 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_bUnion_card_iff_exists_injective'is Hall's theorem with a finite index set. This is elsewhere generalized tofinset.all_card_le_bUnion_card_iff_exists_injective.
Tags #
Hall's Marriage Theorem, indexed families
First case of the inductive step: assuming that
∀ (s : finset ι), s.nonempty → s ≠ univ → s.card < (s.bUnion 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.bUnion 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_bUnion_card_iff_exists_injective for a version
where the finite ι constraint is removed.