intro z hz
case h.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
⊢ ∀ i ∈ K, IsClosed {x | x i ∈ Q K}
case h.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
z : ℂ
hz : z ∈ K
⊢ IsClosed {x | x z ∈ Q K}