F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
f : ℝ → F
K : Set F
inst✝¹ : CompleteSpace F
inst✝ : SecondCountableTopology F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
⊢ StronglyMeasurable fun x => derivWithin f (Ioi x) x
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
f : ℝ → F
K : Set F
inst✝¹ : CompleteSpace F
inst✝ : SecondCountableTopology F
⊢ StronglyMeasurable fun x => derivWithin f (Ioi x) x
borelize F
no goals
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
f : ℝ → F
K : Set F
inst✝¹ : CompleteSpace F
inst✝ : SecondCountableTopology F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
⊢ StronglyMeasurable fun x => derivWithin f (Ioi x) x
exact (measurable_derivWithin_Ioi f).stronglyMeasurable