English
A full strong induction proof of Hall's Marriage Theorem, combining the two inductive steps A and B to establish the existence of a transversal for any finite index set ι.
Русский
Полное сильное доказательство Холла: объединение двух индуктивных шагов A и B даёт существование трансверсала для любого конечного множества индексов ι.
LaTeX
$$$\\exists f: ι \\to α, \\text{Injective}(f) \\wedge \\forall x, f(x) \\in t(x).$$$
Lean4
/-- Here we combine the two inductive steps into a full strong induction proof,
completing the proof the harder direction of **Hall's Marriage Theorem**.
-/
theorem hall_hard_inductive (ht : ∀ s : Finset ι, #s ≤ #(s.biUnion t)) :
∃ f : ι → α, Function.Injective f ∧ ∀ x, f x ∈ t x :=
by
cases nonempty_fintype ι
generalize hn : Fintype.card ι = m
induction m using Nat.strongRecOn generalizing ι with
| ind n ih => _
rcases n with (_ | n)
· rw [Fintype.card_eq_zero_iff] at hn
exact ⟨isEmptyElim, isEmptyElim, isEmptyElim⟩
· have ih' :
∀ (ι' : Type u) [Fintype ι'] (t' : ι' → Finset α),
Fintype.card ι' ≤ n →
(∀ s' : Finset ι', #s' ≤ #(s'.biUnion t')) → ∃ f : ι' → α, Function.Injective f ∧ ∀ x, f x ∈ t' x :=
by
intro ι' _ _ hι' ht'
exact ih _ (Nat.lt_succ_of_le hι') ht' _ rfl
by_cases h : ∀ s : Finset ι, s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
· refine hall_hard_inductive_step_A hn ht (@fun ι' => ih' ι') h
· push_neg at h
rcases h with ⟨s, sne, snu, sle⟩
exact hall_hard_inductive_step_B hn ht (@fun ι' => ih' ι') s sne snu (Nat.le_antisymm (ht _) sle)
