English
If a differentiable function has zero derivative everywhere, then it is constant on the whole domain.
Русский
Если дифференцируемая функция имеет нулевую производную во всех точках, она константна на всей области.
LaTeX
$$$f\text{ differentiable on }E\text{ and }f'(x)=0\text{ for all }x\in E\quad\Rightarrow\quad f\text{ is constant on }E.$$$
Lean4
/-- If two functions have equal Fréchet derivatives at every point of a convex set, and are equal at
one point in that set, then they are equal on that set. -/
theorem eqOn_of_fderivWithin_eq (hs : Convex ℝ s) (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s)
(hs' : UniqueDiffOn 𝕜 s) (hf' : s.EqOn (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s)) (hx : x ∈ s) (hfgx : f x = g x) :
s.EqOn f g := fun y hy =>
by
suffices f x - g x = f y - g y by rwa [hfgx, sub_self, eq_comm, sub_eq_zero] at this
refine hs.is_const_of_fderivWithin_eq_zero (hf.sub hg) (fun z hz => ?_) hx hy
rw [fderivWithin_sub (hs' _ hz) (hf _ hz) (hg _ hz), sub_eq_zero, hf' hz]
