mathlib documentation

combinatorics.hall.finite

Hall's Marriage Theorem for finite index types #

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 a fintype. The combinatorics.hall.basic module applies a compactness argument to this version to remove the fintype 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 #

Tags #

Hall's Marriage Theorem, indexed families

theorem hall_marriage_theorem.hall_hard_inductive_zero {ι : Type u} {α : Type v} [fintype ι] (t : ι → finset α) (hn : fintype.card ι = 0) :
∃ (f : ι → α), function.injective f ∀ (x : ι), f x t x
theorem hall_marriage_theorem.hall_cond_of_erase {ι : Type u} {α : Type v} [fintype ι] {t : ι → finset α} [decidable_eq α] {x : ι} (a : α) (ha : ∀ (s : finset ι), s.nonemptys finset.univs.card < (s.bUnion t).card) (s' : finset {x' : ι | x' x}) :
s'.card (s'.bUnion (λ (x' : {x' : ι | x' x}), (t x').erase a)).card
theorem hall_marriage_theorem.hall_hard_inductive_step_A {ι : Type u} {α : Type v} [fintype ι] {t : ι → finset α} [decidable_eq α] {n : } (hn : fintype.card ι = n + 1) (ht : ∀ (s : finset ι), s.card (s.bUnion t).card) (ih : ∀ {ι' : Type u} [_inst_3 : fintype ι'] (t' : ι' → finset α), fintype.card ι' n(∀ (s' : finset ι'), s'.card (s'.bUnion t').card)(∃ (f : ι' → α), function.injective f ∀ (x : ι'), f x t' x)) (ha : ∀ (s : finset ι), s.nonemptys finset.univs.card < (s.bUnion t).card) :
∃ (f : ι → α), function.injective f ∀ (x : ι), f x t x

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.

theorem hall_marriage_theorem.hall_cond_of_restrict {α : Type v} [decidable_eq α] {ι : Type u} {t : ι → finset α} {s : finset ι} (ht : ∀ (s : finset ι), s.card (s.bUnion t).card) (s' : finset s) :
s'.card (s'.bUnion (λ (a' : s), t a')).card
theorem hall_marriage_theorem.hall_cond_of_compl {α : Type v} [decidable_eq α] {ι : Type u} {t : ι → finset α} {s : finset ι} (hus : s.card = (s.bUnion t).card) (ht : ∀ (s : finset ι), s.card (s.bUnion t).card) (s' : finset (s)) :
s'.card (s'.bUnion (λ (x' : (s)), t x' \ s.bUnion t)).card
theorem hall_marriage_theorem.hall_hard_inductive_step_B {ι : Type u} {α : Type v} [fintype ι] {t : ι → finset α} [decidable_eq α] {n : } (hn : fintype.card ι = n + 1) (ht : ∀ (s : finset ι), s.card (s.bUnion t).card) (ih : ∀ {ι' : Type u} [_inst_3 : fintype ι'] (t' : ι' → finset α), fintype.card ι' n(∀ (s' : finset ι'), s'.card (s'.bUnion t').card)(∃ (f : ι' → α), function.injective f ∀ (x : ι'), f x t' x)) (s : finset ι) (hs : s.nonempty) (hns : s finset.univ) (hus : s.card = (s.bUnion t).card) :
∃ (f : ι → α), function.injective f ∀ (x : ι), f x t x

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.

theorem hall_marriage_theorem.hall_hard_inductive_step {ι : Type u} {α : Type v} [fintype ι] {t : ι → finset α} [decidable_eq α] {n : } (hn : fintype.card ι = n + 1) (ht : ∀ (s : finset ι), s.card (s.bUnion t).card) (ih : ∀ {ι' : Type u} [_inst_3 : fintype ι'] (t' : ι' → finset α), fintype.card ι' n(∀ (s' : finset ι'), s'.card (s'.bUnion t').card)(∃ (f : ι' → α), function.injective f ∀ (x : ι'), f x t' x)) :
∃ (f : ι → α), function.injective f ∀ (x : ι), f x t x

If ι has cardinality n + 1 and the statement of Hall's Marriage Theorem is true for all ι' of cardinality ≤ n, then it is true for ι.

theorem hall_marriage_theorem.hall_hard_inductive {ι : Type u} {α : Type v} [fintype ι] {t : ι → finset α} [decidable_eq α] {n : } (hn : fintype.card ι = n) (ht : ∀ (s : finset ι), s.card (s.bUnion t).card) :
∃ (f : ι → α), function.injective f ∀ (x : ι), f x t x

Here we combine the base case and the inductive step into a full strong induction proof, thus completing the proof of the second direction.

theorem finset.all_card_le_bUnion_card_iff_exists_injective' {ι : Type u_1} {α : Type u_2} [fintype ι] [decidable_eq α] (t : ι → finset α) :
(∀ (s : finset ι), s.card (s.bUnion t).card) ∃ (f : ι → α), function.injective 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 α with ι a fintype. 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 fintype ι constraint is removed.