English
If a differentiable-on segment function has derivWithin equal to zero on the interior, then it is constant on the segment.
Русский
Если derivWithin равна нулю внутри отрезка, функция константна по этому отрезку.
LaTeX
$$$\text{DifferentiableOn } f \ wedge \forall x\in I^{o},\ derivWithin f( Icc, x)=0 \Rightarrow f\text{ constant on }Icc.$$$
Lean4
/-- If two continuous functions on `[a, b]` have the same right derivative and are equal at `a`,
then they are equal everywhere on `[a, b]`. -/
theorem eq_of_has_deriv_right_eq (derivf : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x)
(derivg : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x) (fcont : ContinuousOn f (Icc a b))
(gcont : ContinuousOn g (Icc a b)) (hi : f a = g a) : ∀ y ∈ Icc a b, f y = g y :=
by
simp only [← @sub_eq_zero _ _ (f _)] at hi ⊢
exact
hi ▸
constant_of_has_deriv_right_zero (fcont.sub gcont) fun y hy => by
simpa only [sub_self] using (derivf y hy).sub (derivg y hy)
