theorem CompactnessArgument.compactness_argument {V : Type u_1} {α : V → Type u_2} [(v : V) → Fintype (α v)] [(v : V) → TopologicalSpace (α v)] [∀ (v : V), DiscreteTopology (α v)] (events : Set (Set ((v : V) → α v))) (hclosed : ∀ A ∈ events, IsClosed Aᶜ) (hfin : ∀ F ⊆ events, F.Finite → ∃ (f : (v : V) → α v), ∀ A ∈ F, f ∉ A) : ∃ (f : (v : V) → α v), ∀ A ∈ events, f ∉ A

Compactness argument (Lemma 6.2.7): if every finite subfamily of bad events can be jointly avoided by some assignment $f : (v : V) \to \alpha\,v$ on a product of finite spaces, then the entire (possibly infinite) family can be jointly avoided.