English
If two functions have the same right derivative on a common interval and agree at the left endpoint, then they are equal on the whole interval.
Русский
Если две функции имеют одинаковую правую производную на общем промежутке и совпадают в начальной точке, то они совпадают на всём промежутке.
LaTeX
$$$\forall x\in[a,b],\ f'(x)\text{ exists and same for both} \Rightarrow f=g\text{ on }[a,b].$$$
Lean4
theorem constant_of_derivWithin_zero (hdiff : DifferentiableOn ℝ f (Icc a b))
(hderiv : ∀ x ∈ Ico a b, derivWithin f (Icc a b) x = 0) : ∀ x ∈ Icc a b, f x = f a :=
by
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
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
