Transversals

TheoremHall's marriage theorem #

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.

Finset.all_card_le_biUnion_card_iff_exists_injective.{u, v} {ι : Type u} {α : Type v}
  [DecidableEq α] (t : ι → Finset α) :
  (∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) ↔ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x