English
There exists a transversal f: α → β (injective and graph within R) iff every subset A ⊆ α is related to at least |A| β-elements via the relation R.
Русский
Существование трансверсала f: α → β (инъективного, график подRelation R) эквивалентно тому, что для каждого подмножества A ⊆ α существует как минимум |A| элементов β, связанныx с A через R.
LaTeX
$$$(\\\\forall A \\\\subseteq α, |A| \\\\le \\\\#R.image(A)) \\\\iff \\\\exists f: α \\\\to β, \\\\text{Injective}(f) \\\\wedge \\\\forall x, x \\\\sim_R f(x).$$$
Lean4
/-- 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; see
`Fintype.all_card_le_filter_rel_iff_exists_injective`). 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 `β`.
Note: if `[Fintype β]`, then there exist instances for `[∀ (a : α), Fintype (R.image {a})]`.
-/
theorem all_card_le_rel_image_card_iff_exists_injective {α : Type u} {β : Type v} [DecidableEq β] (R : SetRel α β)
[∀ a : α, Fintype (R.image { a })] :
(∀ A : Finset α, #A ≤ Fintype.card (R.image A)) ↔ ∃ f : α → β, Function.Injective f ∧ ∀ x, x ~[R] f x :=
by
let r' a := (R.image { a }).toFinset
have h : ∀ A : Finset α, Fintype.card (R.image A) = #(A.biUnion r') :=
by
intro A
rw [← Set.toFinset_card]
apply congr_arg
ext b
simp [r', SetRel.image]
have h' : ∀ (f : α → β) (x), x ~[R] f x ↔ f x ∈ r' x := by simp [r', SetRel.image]
simp only [h, h']
apply Finset.all_card_le_biUnion_card_iff_exists_injective
