# mathlibdocumentation

combinatorics.hall

# 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

theorem hall_marriage_theorem.hall_hard_inductive_zero {ι : Type u} {α : Type v} [fintype ι] (t : ι → ) (hn : = 0) :
∃ (f : ι → α), ∀ (x : ι), f x t x
theorem hall_marriage_theorem.hall_cond_of_erase {ι : Type u} {α : Type v} [fintype ι] {t : ι → } [decidable_eq α] {x : ι} (a : α) (ha : ∀ (s : finset ι), s.nonemptys.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 : ι → } [decidable_eq α] {n : } (hn : = n + 1) (ht : ∀ (s : finset ι), s.card (s.bUnion t).card) (ih : ∀ {ι' : Type u} [_inst_3 : fintype ι'] (t' : ι' → finset α), n(∀ (s' : finset ι'), s'.card (s'.bUnion t').card)(∃ (f : ι' → α), ∀ (x : ι'), f x t' x)) (ha : ∀ (s : finset ι), s.nonemptys.card < (s.bUnion t).card) :
∃ (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 : ι → } {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 : ι → } {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 : ι → } [decidable_eq α] {n : } (hn : = n + 1) (ht : ∀ (s : finset ι), s.card (s.bUnion t).card) (ih : ∀ {ι' : Type u} [_inst_3 : fintype ι'] (t' : ι' → finset α), n(∀ (s' : finset ι'), s'.card (s'.bUnion t').card)(∃ (f : ι' → α), ∀ (x : ι'), f x t' x)) (s : finset ι) (hs : s.nonempty) (hns : s finset.univ) (hus : s.card = (s.bUnion t).card) :
∃ (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 : ι → } [decidable_eq α] {n : } (hn : = n + 1) (ht : ∀ (s : finset ι), s.card (s.bUnion t).card) (ih : ∀ {ι' : Type u} [_inst_3 : fintype ι'] (t' : ι' → finset α), n(∀ (s' : finset ι'), s'.card (s'.bUnion t').card)(∃ (f : ι' → α), ∀ (x : ι'), f x t' x)) :
∃ (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 : ι → } [decidable_eq α] {n : } (hn : = n) (ht : ∀ (s : finset ι), s.card (s.bUnion t).card) :
∃ (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 : ι → ) :
(∀ (s : finset ι), s.card (s.bUnion t).card) ∃ (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.

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

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

Equations
theorem fintype.all_card_le_rel_image_card_iff_exists_injective {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (r : α → β → Prop) [Π (a : α), fintype {a})] :
(∀ (A : finset α), A.card fintype.card A)) ∃ (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.

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 : α → β), ∀ (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.