English
If a function has zero Fréchet derivative on a convex set, then it is constant on that set.
Русский
Если функция имеет ноль Фреше производной на выпуклом множестве, то она константа на этом множестве.
LaTeX
$$$\text{If } f:\;E\to G\text{ is differentiable on }s\subset E,\ f'(x)=0\text{ for all }x\in s,\text{ then }f\text{ is constant on }s.$$$
Lean4
/-- If a function has zero Fréchet derivative at every point of a convex set,
then it is a constant on this set. -/
theorem is_const_of_fderivWithin_eq_zero (hs : Convex ℝ s) (hf : DifferentiableOn 𝕜 f s)
(hf' : ∀ x ∈ s, fderivWithin 𝕜 f s x = 0) (hx : x ∈ s) (hy : y ∈ s) : f x = f y :=
by
have bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖ ≤ 0 := fun x hx => by simp only [hf' x hx, norm_zero, le_rfl]
simpa only [(dist_eq_norm _ _).symm, zero_mul, dist_le_zero, eq_comm] using
hs.norm_image_sub_le_of_norm_fderivWithin_le hf bound hx hy
