rintro f -
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ ContinuousOn uderiv (𝓗 U)
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ ContinuousWithinAt uderiv (𝓗 U) f