English
Second inductive step: from the Hall condition and the inductive hypothesis, deduce existence of a transversal by combining two restricted constructions.
Русский
Второй индуктивный шаг: из условия Холла и гипотезы индукции получить трансверсал, объединяя две ограниченные конструкции.
LaTeX
$$$\\text{Given } ht,\\; ih,\\; s,\\; hs,\\; hus,\\; \\text{there exists } f: ι \\to α \\text{ with } f(i) ∈ t(i).$$$
Lean4
/-- Second case of the inductive step: assuming that
`∃ (s : Finset ι), 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_B {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)
(s : Finset ι) (hs : s.Nonempty) (hns : s ≠ univ) (hus : #s = #(s.biUnion t)) :
∃ f : ι → α, Function.Injective f ∧ ∀ x, f x ∈ t x :=
by
haveI := Classical.decEq ι
rw [Nat.add_one] at hn
have card_ι'_le : Fintype.card s ≤ n := by
apply Nat.le_of_lt_succ
calc
Fintype.card s = #s := Fintype.card_coe _
_ < Fintype.card ι := ((card_lt_iff_ne_univ _).mpr hns)
_ = n.succ := hn
let t' : s → Finset α := fun x' => t x'
rcases ih t' card_ι'_le (hall_cond_of_restrict ht) with
⟨f', hf', hsf'⟩
-- Restrict to `sᶜ` in the domain and `(s.biUnion t)ᶜ` in the codomain.
set ι'' := (s : Set ι)ᶜ
let t'' : ι'' → Finset α := fun a'' => t a'' \ s.biUnion t
have card_ι''_le : Fintype.card ι'' ≤ n :=
by
simp_rw [ι'', ← Nat.lt_succ_iff, ← hn, ← Finset.coe_compl, coe_sort_coe]
rwa [Fintype.card_coe, card_compl_lt_iff_nonempty]
rcases ih t'' card_ι''_le (hall_cond_of_compl hus ht) with
⟨f'', hf'', hsf''⟩
-- Put them together
have f''_notMem_biUnion : ∀ (x'') (hx'' : x'' ∉ s), f'' ⟨x'', hx''⟩ ∉ s.biUnion t :=
by
intro x'' hx''
have h := hsf'' ⟨x'', hx''⟩
rw [mem_sdiff] at h
exact h.2
have im_disj : ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s), f' ⟨x', hx'⟩ ≠ f'' ⟨x'', hx''⟩ := by grind
refine ⟨fun x => if h : x ∈ s then f' ⟨x, h⟩ else f'' ⟨x, h⟩, ?_, ?_⟩
· refine hf'.dite _ hf'' (@fun x x' => im_disj x x' _ _)
· intro x
simp only
split_ifs with h
· exact hsf' ⟨x, h⟩
· exact sdiff_subset (hsf'' ⟨x, h⟩)
