E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.49446
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
hdiff : DifferentiableOn ℝ f (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ico a b → derivWithin f (Icc a b) x = 0
H : ∀ (x : ℝ), x ∈ Ico a b → ‖derivWithin f (Icc a b) x‖ ≤ 0
⊢ ∀ (x : ℝ), x ∈ Icc a b → f x = f a
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.49446
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
hdiff : DifferentiableOn ℝ f (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ico a b → derivWithin f (Icc a b) x = 0
⊢ ∀ (x : ℝ), x ∈ Icc a b → f x = f a
have H : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ 0 := by
  simpa only [norm_le_zero_iff] using fun x hx => hderiv x hx
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.49446
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
hdiff : DifferentiableOn ℝ f (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ico a b → derivWithin f (Icc a b) x = 0
H : ∀ (x : ℝ), x ∈ Ico a b → ‖derivWithin f (Icc a b) x‖ ≤ 0
⊢ ∀ (x : ℝ), x ∈ Icc a b → f x = f a
simpa only [zero_mul, norm_le_zero_iff, sub_eq_zero] using fun x hx =>
  norm_image_sub_le_of_norm_deriv_le_segment hdiff H x hx
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.49446
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
hdiff : DifferentiableOn ℝ f (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ico a b → derivWithin f (Icc a b) x = 0
⊢ ∀ (x : ℝ), x ∈ Ico a b → ‖derivWithin f (Icc a b) x‖ ≤ 0
simpa only [norm_le_zero_iff] using fun x hx => hderiv x hx