intro K hK
case h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ ∀ i ∈ compacts U, IsClosed (⋂ i_1 ∈ i, {x | x i_1 ∈ Q i})
case h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
⊢ IsClosed (⋂ i ∈ K, {x | x i ∈ Q K})