English
If differentiable f,g on all E have equal derivatives everywhere, then f = g on E given f and g coincide at least at some point.
Русский
Если гладкие функции f и g на всей области имеют одинаковые производные повсюду и совпадают в хотя бы одной точке, то f = g на всей области.
LaTeX
$$$Differentiable 𝕜 f \\Rightarrow Differentiable 𝕜 g \\Rightarrow (∀ x, fderiv 𝕜 f x = fderiv 𝕜 g x) \\Rightarrow \\\\forall x, f x = g x \\\\Rightarrow f = g$$$
Lean4
theorem _root_.eq_of_fderiv_eq {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : E → G}
(hf : Differentiable 𝕜 f) (hg : Differentiable 𝕜 g) (hf' : ∀ x, fderiv 𝕜 f x = fderiv 𝕜 g x) (x : E)
(hfgx : f x = g x) : f = g := by
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
let A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E
suffices Set.univ.EqOn f g from funext fun x => this <| mem_univ x
exact
convex_univ.eqOn_of_fderivWithin_eq hf.differentiableOn hg.differentiableOn uniqueDiffOn_univ
(fun x _ => by simpa using hf' _) (mem_univ _) hfgx
