Theorem: isCompact_𝓜 (RMT4/Montel.lean)

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
⊢ IsCompact (𝓜 U)
Tactic:
simpa only [𝓑_const] using isCompact_𝓑 hU (fun _ _ => isCompact_closedBall 0 1)
State after:
no goals