English
For a finite β and a relation r, there is an injective transversal f with r x (f x) iff the finite-universal filter condition holds via the Finset.filter construction.
Русский
Для конечной β и отношения r существует инъективный трансверсал f с r x (f x) тогда, когда конечная проверка через Finset.filter удовлетворяет условию Холла.
LaTeX
$$$(\\\\forall A, \\\\#A \\\\le \\\\#\\\\{b \\\\mid \\\\exists a \\\\in A, r a b\\\\}) \\\\iff \\\\exists f: α \\\\to β, \\\\text{Injective}(f) \\\\wedge \\\\forall x, r(x, f(x)).$$$
Lean4
/-- This is a version of **Hall's Marriage Theorem** in terms of a relation to a finite type.
There is a transversal of the relation (an injective function `α → β` whose graph is a subrelation
of 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`.
-/
theorem all_card_le_filter_rel_iff_exists_injective {α : Type u} {β : Type v} [Fintype β] (r : α → β → Prop)
[DecidableRel r] : (∀ A : Finset α, #A ≤ #{b | ∃ a ∈ A, r a b}) ↔ ∃ f : α → β, Injective f ∧ ∀ x, r x (f x) :=
by
haveI := Classical.decEq β
let r' a : Finset β := {b | r a b}
have h : ∀ A : Finset α, ({b | ∃ a ∈ A, r a b} : Finset _) = A.biUnion r' :=
by
intro A
ext b
simp [r']
have h' : ∀ (f : α → β) (x), r x (f x) ↔ f x ∈ r' x := by simp [r']
simp_rw [h, h']
apply Finset.all_card_le_biUnion_card_iff_exists_injective
