English
For indexed finite family t: ι → Finset α, the Hall condition (every subset s satisfies |s| ≤ |s.biUnion t|) is equivalent to the existence of an injective f: ι → α with f(i) ∈ t(i) for all i.
Русский
Для индексированной конечной семейства t: ι → Finset α условие Халла (для любого подмножества s выполняется |s| ≤ |⋃_{i∈s} t(i)|) эквивалентно существованию инъективного отображения f: ι → α с f(i) ∈ t(i) для всех i.
LaTeX
$$$(\\\\forall s \\\\subseteq ι,\#s \\\\le \\\\#(s \\\\ biUnion t)) \\\\iff \\\\exists f: ι \\\\to α, \\\\text{Injective}(f) \\\\wedge \\\\forall x, f(x) \\\\in t(x).$$$
Lean4
/-- 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`.
-/
theorem all_card_le_biUnion_card_iff_exists_injective {ι : Type u} {α : Type v} [DecidableEq α] (t : ι → Finset α) :
(∀ s : Finset ι, #s ≤ #(s.biUnion t)) ↔ ∃ f : ι → α, Function.Injective f ∧ ∀ x, f x ∈ t x :=
by
constructor
· intro h
haveI : ∀ ι' : (Finset ι)ᵒᵖ, Nonempty ((hallMatchingsFunctor t).obj ι') := fun ι' =>
hallMatchingsOn.nonempty t h ι'.unop
classical
haveI : ∀ ι' : (Finset ι)ᵒᵖ, Finite ((hallMatchingsFunctor t).obj ι') :=
by
intro ι'
rw [hallMatchingsFunctor]
infer_instance
-- Apply the compactness argument
obtain ⟨u, hu⟩ :=
nonempty_sections_of_finite_inverse_system
(hallMatchingsFunctor t)
-- Interpret the resulting section of the inverse limit
refine ⟨?_, ?_, ?_⟩
· -- Build the matching function from the section
exact fun i => (u (Opposite.op ({ i } : Finset ι))).val ⟨i, by simp only [mem_singleton]⟩
· -- Show that it is injective
intro i i'
have subi : ({ i } : Finset ι) ⊆ { i, i' } := by simp
have subi' : ({ i' } : Finset ι) ⊆ { i, i' } := by simp
rw [← Finset.le_iff_subset] at subi subi'
simp only
rw [← hu (CategoryTheory.homOfLE subi).op, ← hu (CategoryTheory.homOfLE subi').op]
let uii' := u (Opposite.op ({ i, i' } : Finset ι))
exact fun h => Subtype.mk_eq_mk.mp (uii'.property.1 h)
· -- Show that it maps each index to the corresponding finite set
intro i
apply (u (Opposite.op ({ i } : Finset ι))).property.2
· -- The reverse direction is a straightforward cardinality argument
rintro ⟨f, hf₁, hf₂⟩ s
rw [← Finset.card_image_of_injective s hf₁]
apply Finset.card_le_card
grind
