no goals
α : Type u
β : Type v
ι✝ : Type ?u.18164
π : ι✝ → Type ?u.18169
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
ι : Type v
hs : IsCompact s
Z : ι → Set α
hZc : ∀ (i : ι), IsClosed (Z i)
hsZ : (s ∩ ⋂ (i : ι), Z i) = ∅
⊢ s ⊆ ⋃ (i : ι), (fun i => Z iᶜ) i
simpa only [subset_def, not_forall, eq_empty_iff_forall_not_mem, mem_iUnion, exists_prop,
  mem_inter_iff, not_and, iff_self_iff, mem_iInter, mem_compl_iff] using hsZ
no goals
α : Type u
β : Type v
ι✝ : Type ?u.18164
π : ι✝ → Type ?u.18169
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
ι : Type v
hs : IsCompact s
Z : ι → Set α
hZc : ∀ (i : ι), IsClosed (Z i)
hsZ : (s ∩ ⋂ (i : ι), Z i) = ∅
t : Finset ι
ht : s ⊆ ⋃ (i : ι) (_ : i ∈ t), Z iᶜ
⊢ (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
simpa only [subset_def, not_forall, eq_empty_iff_forall_not_mem, mem_iUnion, exists_prop,
mem_inter_iff, not_and, iff_self_iff, mem_iInter, mem_compl_iff] using ht