exact h.continuousOn_derivWithin (uniqueDiffOn_Icc hab) le_rfl
case hint
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a < b
⊢ ContinuousOn (fun y => derivWithin f (Icc a b) y) (Icc a b)
no goals