is_const_of_deriv_eq_zero — Mathlib

English

If two differentiable functions have equal derivatives on an open convex set, then they differ by a constant shift on that set.

Русский

Если две дифференцируемые функции имеют равные производные на открытом выпуклом множестве, они отличаются на константное сдвиг.

LaTeX

$$$$ f(x) = g(x) + a, \text{ for all } x \in s $$$$

Lean4

theorem _root_.IsOpen.is_const_of_deriv_eq_zero (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s)
    (hf' : s.EqOn (deriv f) 0) {x y : 𝕜} (hx : x ∈ s) (hy : y ∈ s) : f x = f y :=
  hs.is_const_of_fderiv_eq_zero hs' hf (fun a ha ↦ by ext; simp [← deriv_fderiv, hf' ha]) hx hy

Похожие утверждения