English
For any family of closed sets whose intersection avoids a compact set, there exists a finite subfamily whose intersection still avoids the compact set.
Русский
Для любой семейства замкнутых множеств, чье пересечение не пересекается с компактным множеством, существует конечная подподсемейство, чье пересечение всё ещё не пересекается с компактным множеством.
LaTeX
$$$IsCompact(s) \rightarrow \forall t: ι \to Set X, (\forall i, IsClosed (t i)) \rightarrow (s \cap \bigcap i, t i) = \emptyset \rightarrow \exists u : Finset ι, (s \cap \bigcap i \in u, t i) = \emptyset$$$
Lean4
/-- For every family of closed sets whose intersection avoids a compact set,
there exists a finite subfamily whose intersection avoids this compact set. -/
theorem elim_finite_subfamily_closed {ι : Type v} (hs : IsCompact s) (t : ι → Set X) (htc : ∀ i, IsClosed (t i))
(hst : (s ∩ ⋂ i, t i) = ∅) : ∃ u : Finset ι, (s ∩ ⋂ i ∈ u, t i) = ∅ :=
hs.elim_directed_family_closed _ (fun _ ↦ isClosed_biInter fun _ _ ↦ htc _) (by rwa [← iInter_eq_iInter_finset])
(directed_of_isDirected_le fun _ _ h ↦ biInter_subset_biInter_left h)
