have l2 (K) (hK : K ∈ compacts U) (x) (hx : x ∈ K) : ∃ L, IsCompact L ∧ ∀ i : 𝓑 U Q, i.1 x ∈ L :=
  ⟨Q K, hQ K hK, fun f => f.2.2 K hK hx⟩
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
⊢ IsCompact (𝓑 U Q)
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ IsCompact (𝓑 U Q)