no goals
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
f : ℝ → F
K : Set F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
⊢ Measurable fun x => derivWithin f (Ioi x) x
simpa [derivWithin_Ioi_eq_Ici] using measurable_derivWithin_Ici f