E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.41030
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b C : ℝ
hf : DifferentiableOn ℝ f (Icc a b)
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖derivWithin f (Icc a b) x‖ ≤ C
⊢ ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt (fun x => f x) (derivWithin f (Icc a b) x) (Icc a b) x
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.41030
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b C : ℝ
hf : DifferentiableOn ℝ f (Icc a b)
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖derivWithin f (Icc a b) x‖ ≤ C
⊢ ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ C * (x - a)
refine' norm_image_sub_le_of_norm_deriv_le_segment' _ bound
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.41030
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b C : ℝ
hf : DifferentiableOn ℝ f (Icc a b)
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖derivWithin f (Icc a b) x‖ ≤ C
⊢ ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt (fun x => f x) (derivWithin f (Icc a b) x) (Icc a b) x
exact fun x hx => (hf x hx).hasDerivWithinAt