Hall's Marriage Theorem #

Given a list of finite subsets $X_1,X_2,\dots,X_n$ of some given set $S$, 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.

This file proves this for an indexed family t : ι → finset α of finite sets, with [fintype ι], along with some variants of the statement. The list of distinct representatives is given by an injective function f : ι → α such that ∀ i, f i ∈ t i.

A description of this formalization is in [GMM].

Main statements #

finset.all_card_le_bUnion_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 theorem is still true even if ι is not a finite type. The infinite case follows from a compactness argument.
The statement of the theorem in terms of bipartite graphs is in preparation.

Tags #

Hall's Marriage Theorem, indexed families

source

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

source

theorem hall_marriage_theorem.hall_cond_of_erase {ι : Type u} {α : Type v} [fintype ι] {t : ι → finset α} [decidable_eq α] {x : ι} (a : α) (ha : ∀ (s : finset ι), s.nonempty → s ≠ finset.univ → s.card < (s.bUnion t).card) (s' : finset ↥{x' : ι | x' ≠ x}) :

s'.card ≤ (s'.bUnion (λ (x' : ↥{x' : ι | x' ≠ x}), (t ↑x').erase a)).card

source

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.nonempty → s ≠ finset.univ → s.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.

source

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

source

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

source

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.

source

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 ι.

source

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.

source

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 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.bUnion t is the union of all the sets t i for i ∈ s.

source

@[protected, instance]

def rel.image.fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] (r : α → β → Prop) [Π (a : α), fintype ↥(rel.image r {a})] (A : finset α) :

fintype ↥(rel.image r ↑A)

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

Equations

rel.image.fintype r A = _.mpr (finset_coe.fintype (A.bUnion (λ (a : α), (rel.image r {a}).to_finset)))

source

theorem fintype.all_card_le_rel_image_card_iff_exists_injective {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (r : α → β → Prop) [Π (a : α), fintype ↥(rel.image r {a})] :

(∀ (A : finset α), A.card ≤ fintype.card ↥(rel.image r ↑A)) ↔ ∃ (f : α → β), function.injective f ∧ ∀ (x : α), r x (f x)

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). There is an injective function α → β respecting the relation iff every subset of k terms of α is related to at least k terms of β.

If [fintype β], then [∀ (a : α), fintype (rel.image r {a})] is automatically implied.

source

theorem fintype.all_card_le_filter_rel_iff_exists_injective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (r : α → β → Prop) [Π (a : α), decidable_pred (r a)] :

(∀ (A : finset α), A.card ≤ (finset.filter (λ (b : β), ∃ (a : α) (H : a ∈ A), r a b) finset.univ).card) ↔ ∃ (f : α → β), function.injective f ∧ ∀ (x : α), r x (f x)

This is a version of Hall's Marriage Theorem in terms of a relation between finite types. There is an injective function α → β respecting 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.