English
If two differentiable functions f and g have equal derivatives on an open, preconnected set s, then there exists a constant a such that f = g + a on s.
Русский
Если две гладкие функции имеют равные производные на открытом и связанном по смыслу множестве s, то существует константа a так, что f = g + a на s.
LaTeX
$$$IsOpen s \\Rightarrow IsPreconnected s \\Rightarrow DifferentiableOn 𝕜 f s \\Rightarrow DifferentiableOn 𝕜 g s \\Rightarrow (∀ x ∈ s, fderiv 𝕜 f x = fderiv 𝕜 f g x) \\Rightarrow ∃ a, s.EqOn f (g · + a)$$$
Lean4
theorem _root_.IsOpen.is_const_of_fderiv_eq_zero (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s)
(hf' : s.EqOn (fderiv 𝕜 f) 0) {x y : E} (hx : x ∈ s) (hy : y ∈ s) : f x = f y :=
by
obtain ⟨a, ha⟩ := hs.exists_is_const_of_fderiv_eq_zero hs' hf hf'
rw [ha x hx, ha y hy]
