exists_eq_add_of_deriv_eq — Mathlib

English

If an open set s has a differentiable function with deriv same as another on s, it is constant on s.

Русский

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

LaTeX

$$$$ f|_{s} = g|_{s} + a, \ a\in G $$$$

Lean4

theorem _root_.IsOpen.exists_eq_add_of_deriv_eq {f g : 𝕜 → G} (hs : IsOpen s) (hs' : IsPreconnected s)
    (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hf' : s.EqOn (deriv f) (deriv g)) :
    ∃ a, s.EqOn f (g · + a) :=
  hs.exists_eq_add_of_fderiv_eq hs' hf hg (fun x hx ↦ by simp [← deriv_fderiv, hf' hx])

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