have hU : IsOpen U := good_domain.is_open
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
⊢ IsCompact (𝓙 U)
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
⊢ IsCompact (𝓙 U)