Theorem: uniformlyBoundedOn_𝓑 (RMT4/Montel.lean)

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ UniformlyBoundedOn Subtype.val U
Tactic:
exact fun K hK => ⟨Q K, hQ K hK, fun f => f.2.2 K hK⟩
State after:
no goals