rintro ⟨z, hz⟩
ι : 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
hK : K ∈ compacts U
⊢ Equicontinuous (restrict K ∘ F)
case mk
ι : 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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }