𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type ?u.404351
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✝ : SecondCountableTopology F
f : 𝕜 → F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
⊢ StronglyMeasurable (deriv f)
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type ?u.404351
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✝ : SecondCountableTopology F
f : 𝕜 → F
⊢ StronglyMeasurable (deriv f)
borelize F
no goals
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type ?u.404351
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✝ : SecondCountableTopology F
f : 𝕜 → F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
⊢ StronglyMeasurable (deriv f)
exact (measurable_deriv f).stronglyMeasurable