English
Inductive step: from the Hall condition and the inductive hypothesis for all smaller index sets, derive the existence of a transversal for a set ι of size n+1.
Русский
Индуктивный шаг: из условия Холла и предположения индукции для всех меньших по размеру множеств ι вывести существование трансверсала для множества ι размером n+1.
LaTeX
$$$\\text{If } ht(s) \\text{ holds and } |ι| = n+1,\\; \\text{then there exists } f: ι \\to α\\text{ with } f\\text{ injective and } f(i) \\in t(i).$$$
Lean4
/-- First case of the inductive step: assuming that
`∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)`
and that the statement of **Hall's Marriage Theorem** is true for all
`ι'` of cardinality ≤ `n`, then it is true for `ι` of cardinality `n + 1`.
-/
theorem hall_hard_inductive_step_A {n : ℕ} (hn : Fintype.card ι = n + 1) (ht : ∀ s : Finset ι, #s ≤ #(s.biUnion t))
(ih :
∀ {ι' : Type u} [Fintype ι'] (t' : ι' → Finset α),
Fintype.card ι' ≤ n →
(∀ s' : Finset ι', #s' ≤ #(s'.biUnion t')) → ∃ f : ι' → α, Function.Injective f ∧ ∀ x, f x ∈ t' x)
(ha : ∀ s : Finset ι, s.Nonempty → s ≠ univ → #s < #(s.biUnion t)) :
∃ f : ι → α, Function.Injective f ∧ ∀ x, f x ∈ t x :=
by
haveI : Nonempty ι := Fintype.card_pos_iff.mp (hn.symm ▸ Nat.succ_pos _)
haveI := Classical.decEq ι
let x := Classical.arbitrary ι
have tx_ne : (t x).Nonempty := by
rw [← Finset.card_pos]
calc
0 < 1 := Nat.one_pos
_ ≤ #(.biUnion { x } t) := (ht { x })
_ = (t x).card := by rw [Finset.singleton_biUnion]
choose y hy using tx_ne
let ι' := {x' : ι | x' ≠ x}
let t' : ι' → Finset α := fun x' => (t x').erase y
have card_ι' : Fintype.card ι' = n :=
calc
Fintype.card ι' = Fintype.card ι - 1 := Set.card_ne_eq _
_ = n := by rw [hn, Nat.add_succ_sub_one, add_zero]
rcases ih t' card_ι'.le (hall_cond_of_erase y ha) with
⟨f', hfinj, hfr⟩
-- Extend the resulting function.
refine ⟨fun z => if h : z = x then y else f' ⟨z, h⟩, ?_, ?_⟩
· rintro z₁ z₂
have key : ∀ {x}, y ≠ f' x := by
intro x h
simpa [t', ← h] using hfr x
by_cases h₁ : z₁ = x <;> by_cases h₂ : z₂ = x <;> simp [h₁, h₂, hfinj.eq_iff, key, key.symm]
· intro z
simp only
split_ifs with hz
· rwa [hz]
· specialize hfr ⟨z, hz⟩
rw [mem_erase] at hfr
exact hfr.2
