English
If a compact set s intersects every finite intersection of a family of closed sets, then the intersection of all the closed sets is nonempty.
Русский
Если компактное множество s пересекает каждую конечную ktoc intersect-через семейством замкнутых множеств, то пересечение всех множеств непусто.
LaTeX
$$$IsCompact(s) \rightarrow (\forall t: Finset ι, (s \cap \bigcap i \in t, t i).Nonempty) \rightarrow (s \cap \bigcap i, t i).Nonempty$$$
Lean4
/-- To show that a compact set intersects the intersection of a family of closed sets,
it is sufficient to show that it intersects every finite subfamily. -/
theorem inter_iInter_nonempty {ι : Type v} (hs : IsCompact s) (t : ι → Set X) (htc : ∀ i, IsClosed (t i))
(hst : ∀ u : Finset ι, (s ∩ ⋂ i ∈ u, t i).Nonempty) : (s ∩ ⋂ i, t i).Nonempty :=
by
contrapose! hst
exact hs.elim_finite_subfamily_closed t htc hst
