English
If the Hall condition holds for s, then the Hall condition holds for the complement subsystem with t(x) removed on s.
Русский
Если условие Холла выполняется для s, то для дополнительной подсистемы с удалением t(x) из s оно также выполняется.
LaTeX
$$$\\forall s, |s| = |\\\\bigcup t| \\\\Rightarrow \\\\forall s',|s'| \\\\le |\\\\bigcup_{x'\\in s'} (t(x')\\setminus s\\\\bigcup t)|.$$$
Lean4
theorem hall_cond_of_compl {ι : Type u} {t : ι → Finset α} {s : Finset ι} (hus : #s = #(s.biUnion t))
(ht : ∀ s : Finset ι, #s ≤ #(s.biUnion t)) (s' : Finset (sᶜ : Set ι)) :
#s' ≤ #(s'.biUnion fun x' => t x' \ s.biUnion t) :=
by
haveI := Classical.decEq ι
have disj : Disjoint s (s'.image fun z => z.1) :=
by
simp only [disjoint_left, not_exists, mem_image, SetCoe.exists, exists_and_right, exists_eq_right]
intro x hx hc _
exact absurd hx hc
have : #s' = #(s ∪ s'.image fun z => z.1) - #s := by
simp [disj, card_image_of_injective _ Subtype.coe_injective, Nat.add_sub_cancel_left]
rw [this, hus]
refine (Nat.sub_le_sub_right (ht _) _).trans ?_
rw [← card_sdiff_of_subset]
· gcongr
intro t
simp only [mem_biUnion, mem_sdiff, not_exists, mem_image, and_imp, mem_union, exists_imp]
rintro x (hx | ⟨x', hx', rfl⟩) rat hs
· exact False.elim <| (hs x) <| And.intro hx rat
· use x', hx', rat, hs
· apply biUnion_subset_biUnion_of_subset_left
apply subset_union_left
