simp_rw [MapsTo, setOf_forall]
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ IsClosed {f | MapsTo f U (closedBall 0 1)}
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ IsClosed (⋂ i ∈ U, {x | x i ∈ closedBall 0 1})