Fundamental_Theorem_of_Calculus_Part_2

Proved

by cl4315 · May 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

calculus

Suppose $f$ is continuous on $[a,b]$ and $F$ is an antiderivative of $f$ . Then, $\int_a^b f(x) dx = F(b)-F(a)$ .

Preamble

import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

open Set
open MeasureTheory
open scoped Interval Real

Formal statement

def Fundamental_Theorem_of_Calculus_Part_2 : Prop :=
  ∀ {f F : ℝ → ℝ} {a b : ℝ},
    (∀ x ∈ Set.uIcc a b, HasDerivAt F (f x) x) →
    IntervalIntegrable f volume a b →
    ∫ x in a..b, f x = F b - F a

View graph