∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v},
  IsCompact s →
    ∀ (t : ι → Set X),
      (∀ (i : ι), IsClosed (t i)) → (∀ (u : Finset ι), (s ∩ ⋂ i ∈ u, t i).Nonempty) → (s ∩ ⋂ i, t i).Nonempty