English
Finite version of Hall's theorem: the all-card inequality over Finset ι is equivalent to the existence of an injective selector f: ι → α with f(i) ∈ t(i).
Русский
Конечная версия теоремы Холла: равенство всех мощностей по подмножствам и существование инъективного выбора.
LaTeX
$$$(\\\\forall s:Finset ι, \\\\#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 α` with `ι` finite.
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_biUnion_card_iff_exists_injective` for a version
where the `Finite ι` constraint is removed.
-/
theorem all_card_le_biUnion_card_iff_existsInjective' {ι α : Type*} [Finite ι] [DecidableEq α] (t : ι → Finset α) :
(∀ s : Finset ι, #s ≤ #(s.biUnion t)) ↔ ∃ f : ι → α, Function.Injective f ∧ ∀ x, f x ∈ t x :=
by
constructor
· exact HallMarriageTheorem.hall_hard_inductive
· rintro ⟨f, hf₁, hf₂⟩ s
rw [← card_image_of_injective s hf₁]
apply card_le_card
intro
rw [mem_image, mem_biUnion]
rintro ⟨x, hx, rfl⟩
exact ⟨x, hx, hf₂ x⟩
