simpa [derivCLM_apply ℝ] using (derivCLM ℝ f).continuous.continuousOn
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
⊢ ContinuousOn (fun x => deriv (⇑f) x) (Set.uIcc a b)
no goals