no goals
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type ?u.401298
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
f✝ : E → F
K : Set (E →L[𝕜] F)
inst✝⁶ : MeasurableSpace E
inst✝⁵ : OpensMeasurableSpace E
inst✝⁴ : CompleteSpace F
inst✝³ : MeasurableSpace 𝕜
inst✝² : OpensMeasurableSpace 𝕜
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : 𝕜 → F
⊢ Measurable (deriv f)
simpa only [fderiv_deriv] using measurable_fderiv_apply_const 𝕜 f 1