have l1 (K) (hK : K ∈ compacts U) : EquicontinuousOn ((↑) : 𝓑 U Q → 𝓒 U) K :=
  (uniformlyBoundedOn_𝓑 hQ).equicontinuousOn hU (fun f => f.2.1) hK
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q 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
⊢ IsCompact (𝓑 U Q)