English
For every directed family of closed sets whose intersection avoids a compact set, there exists an index i with the intersection with the compact set empty.
Русский
Для каждой направленной фамилии замкнутых множеств, чье пересечение не пересекается с компактным множеством, существует индекс i, для которого s ∩ t_i = ∅.
LaTeX
$$$IsCompact(s) \rightarrow \forall t: ι \to Set X, (\forall i, IsClosed (t i)) \rightarrow (s \cap \bigcap i, t i) = \emptyset \rightarrow Directed (· \supseteq ·) t \rightarrow \exists i, s \cap t i = \emptyset$$$
Lean4
/-- For every directed family of closed sets whose intersection avoids a compact set,
there exists a single element of the family which itself avoids this compact set. -/
theorem elim_directed_family_closed {ι : Type v} [Nonempty ι] (hs : IsCompact s) (t : ι → Set X)
(htc : ∀ i, IsClosed (t i)) (hst : (s ∩ ⋂ i, t i) = ∅) (hdt : Directed (· ⊇ ·) t) : ∃ i : ι, s ∩ t i = ∅ :=
let ⟨t, ht⟩ :=
hs.elim_directed_cover (compl ∘ t) (fun i => (htc i).isOpen_compl)
(by
simpa only [subset_def, not_forall, eq_empty_iff_forall_notMem, mem_iUnion, exists_prop, mem_inter_iff, not_and,
mem_iInter, mem_compl_iff] using hst)
(hdt.mono_comp _ fun _ _ => compl_subset_compl.mpr)
⟨t, by
simpa only [subset_def, not_forall, eq_empty_iff_forall_notMem, mem_iUnion, exists_prop, mem_inter_iff, not_and,
mem_iInter, mem_compl_iff] using ht⟩
-- TODO: reformulate using `Disjoint`
