English
If the Hall condition holds on a set of indices ι, then it also holds for any finite subset s of ι when viewed in terms of the restricted family t restricted to s.
Русский
Если условие Холла выполняется на множестве индексов ι, то оно сохраняется и для любого конечного поднабора s внутри ι для ограниченной семействa t.
LaTeX
$$$\\forall s: \\\\text{Finset }(s: Set ι),\\; |s| \\le |\\\\bigcup_{i\\in s} t(i)| \\\\Rightarrow \\\\text{same for restricted } s.$$$
Lean4
theorem hall_cond_of_restrict {ι : Type u} {t : ι → Finset α} {s : Finset ι} (ht : ∀ s : Finset ι, #s ≤ #(s.biUnion t))
(s' : Finset (s : Set ι)) : #s' ≤ #(s'.biUnion fun a' => t a') := by
classical
rw [← card_image_of_injective s' Subtype.coe_injective]
convert ht (s'.image fun z => z.1) using 1
apply congr_arg
ext y
simp
