English
Let f and g be differentiable on the closed interval [a,b], and suppose their derivatives agree on the half-open interval [a,b) in the sense that derivateWithin f (Icc a b) and derivWithin g (Icc a b) coincide on Ico a b; if f(a) = g(a), then f and g coincide on the entire interval [a,b].
Русский
Пусть f и g дифференцируемы на замкнутом отрезке [a,b], и предположим, что их производные совпадают внутри [a,b) в смысле derivWithin f (Icc a b) = derivWithin g (Icc a b) на Ico a b; если f(a) = g(a), тогда f(y) = g(y) для всех y ∈ [a,b].
LaTeX
$$$\forall y \in [a,b],\ f(y)=g(y) \\text{whenever }\ f,g: \mathbb{R} \to E,\ f,g \text{ differentiable on } [a,b],\\ EqOn(\mathrm{derivWithin}(f,[a,b]), \mathrm{derivWithin}(g,[a,b]))(Ico\,a\,b)\text{ and } f(a)=g(a).$$$
Lean4
/-- If two differentiable functions on `[a, b]` have the same derivative within `[a, b]` everywhere
on `[a, b)` and are equal at `a`, then they are equal everywhere on `[a, b]`. -/
theorem eq_of_derivWithin_eq (fdiff : DifferentiableOn ℝ f (Icc a b)) (gdiff : DifferentiableOn ℝ g (Icc a b))
(hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)) (hi : f a = g a) :
∀ y ∈ Icc a b, f y = g y :=
by
have A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y := fun y hy =>
(fdiff y (mem_Icc_of_Ico hy)).hasDerivWithinAt.mono_of_mem_nhdsWithin (Icc_mem_nhdsGE_of_mem hy)
have B : ∀ y ∈ Ico a b, HasDerivWithinAt g (derivWithin g (Icc a b) y) (Ici y) y := fun y hy =>
(gdiff y (mem_Icc_of_Ico hy)).hasDerivWithinAt.mono_of_mem_nhdsWithin (Icc_mem_nhdsGE_of_mem hy)
exact eq_of_has_deriv_right_eq A (fun y hy => (hderiv hy).symm ▸ B y hy) fdiff.continuousOn gdiff.continuousOn hi
