Primitives_Differ_by_Constant
Provedantiderivativescalculusintegrationproofwiki
If F and G are both primitives of the same function on [a,b], then G = F + c for some constant c.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.MeanValue
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.MeanValue theorem Primitives_Differ_by_Constant (F G : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hF : ContinuousOn F (Set.Icc a b)) (hG : ContinuousOn G (Set.Icc a b)) (hFG : ∀ x ∈ Set.Ioo a b, deriv F x = deriv G x) (hFd : DifferentiableOn ℝ F (Set.Ioo a b)) (hGd : DifferentiableOn ℝ G (Set.Ioo a b)) : ∃ c : ℝ, ∀ x ∈ Set.Icc a b, G x = F x + c := by sorry
Source