English
If a function is differentiable on a segment and its right-derivative is identically zero, then the function is constant on the segment.
Русский
Если функция дифференцируема на отрезке и правая производная по направлению равна нулю, функция константна на отрезке.
LaTeX
$$$\text{DifferentiableOn}(f, [a,b])\land \forall x\in [a,b),\ deriv\ f\ x = 0\Rightarrow f\text{ constant on }[a,b].$$$
Lean4
theorem constant_of_has_deriv_right_zero (hcont : ContinuousOn f (Icc a b))
(hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt f 0 (Ici x) x) : ∀ x ∈ Icc a b, f x = f a :=
by
have : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ 0 * (x - a) := fun x hx =>
norm_image_sub_le_of_norm_deriv_right_le_segment hcont hderiv (fun _ _ => norm_zero.le) x hx
simpa only [zero_mul, norm_le_zero_iff, sub_eq_zero] using this
