English
If the Hall condition holds for a finite index set ι, then there exists a matching f: ι → α with f(i) ∈ t(i) and injective.
Русский
Если выполняется условие Халла для конечного множества индексов ι, то существует матчинговая функция f: ι → α такая, что f(i) ∈ t(i) и отображение инъективно.
LaTeX
$$$\\\\text{If } ht \\\\colon \\\\forall s \\\\subseteq ι, |s| \\\\le |\\\\bigcup_{i\\\\in s} t(i)|, \\\\text{then } \\\\exists f: ι \\\\to α, \\\\text{Injective}(f) \\\\wedge \\\\forall i \\\\in ι, f(i) \\\\in t(i).$$$
Lean4
/-- When the Hall condition is satisfied, the set of matchings on a finite set is nonempty.
This is where `Finset.all_card_le_biUnion_card_iff_existsInjective'` comes into the argument. -/
theorem nonempty {ι : Type u} {α : Type v} [DecidableEq α] (t : ι → Finset α) (h : ∀ s : Finset ι, #s ≤ #(s.biUnion t))
(ι' : Finset ι) : Nonempty (hallMatchingsOn t ι') := by
classical
refine ⟨Classical.indefiniteDescription _ ?_⟩
apply (all_card_le_biUnion_card_iff_existsInjective' fun i : ι' => t i).mp
intro s'
convert h (s'.image (↑)) using 1
· simp only [card_image_of_injective s' Subtype.coe_injective]
· rw [image_biUnion]
