rintro K ⟨hK1, hK2⟩
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
⊢ UniformlyBoundedOn (_root_.deriv ∘ F) U
case intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
⊢ ∃ Q, IsCompact Q ∧ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K Q