English
If differentiable f,g on a connected open set have equal derivatives at every point, and they agree at some point, then f = g on that set.
Русский
Если гладкие функции f и g на связном открытом множестве имеют равные производные в каждой точке и совпадают в одной точке, то они совпадают на всем множестве.
LaTeX
$$$IsOpen s \\Rightarrow IsPreconnected s \\Rightarrow DifferentiableOn 𝕜 f s \\Rightarrow DifferentiableOn 𝕜 g s \\Rightarrow (fderiv 𝕜 f x = fderiv 𝕜 g x) \\\\forall x ∈ s \\\\Rightarrow f x = g x \\\\Rightarrow f = g$$$
Lean4
theorem _root_.IsOpen.exists_eq_add_of_fderiv_eq (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s)
(hg : DifferentiableOn 𝕜 g s) (hf' : s.EqOn (fderiv 𝕜 f) (fderiv 𝕜 g)) : ∃ a, s.EqOn f (g · + a) :=
by
simp_rw [Set.EqOn, ← sub_eq_iff_eq_add']
refine hs.exists_is_const_of_fderiv_eq_zero hs' (hf.sub hg) fun x hx ↦ ?_
rw [fderiv_fun_sub (hf.differentiableAt (hs.mem_nhds hx)) (hg.differentiableAt (hs.mem_nhds hx)), hf' hx, sub_self,
Pi.zero_apply]
