English
If the derivatives of two differentiable functions f and g agree on a connected open set and they agree at a point, then f and g are equal on that set.
Русский
Если производные двух гладких функций согласованы на связанном открытом множестве и они совпадают в одной точке, то функции совпадают на этом множестве.
LaTeX
$$$IsOpen s \\Rightarrow IsPreconnected s \\Rightarrow DifferentiableOn 𝕜 f s \\Rightarrow DifferentiableOn 𝕜 g s \\Rightarrow (∀ x, fderiv 𝕜 f x = fderiv 𝕜 g x) \\Rightarrow (x ∈ s) \\Rightarrow f x = g x \\Rightarrow s.EqOn f g$$$
Lean4
/-- If two functions have equal Fréchet derivatives at every point of a connected open set,
and are equal at one point in that set, then they are equal on that set. -/
theorem _root_.IsOpen.eqOn_of_fderiv_eq (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s)
(hg : DifferentiableOn 𝕜 g s) (hf' : ∀ x ∈ s, fderiv 𝕜 f x = fderiv 𝕜 g x) (hx : x ∈ s) (hfgx : f x = g x) :
s.EqOn f g := by
obtain ⟨a, ha⟩ := hs.exists_eq_add_of_fderiv_eq hs' hf hg hf'
obtain rfl := left_eq_add.mp (hfgx.symm.trans (ha hx))
simpa using ha
