ι : Type ?u.1862127
𝕜 : Type ?u.1862130
E : Type u_1
F : Type ?u.1862136
A : Type ?u.1862139
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ IntervalIntegrable (deriv f) volume a b
ι : Type ?u.1862127
𝕜 : Type ?u.1862130
E : Type u_1
F : Type ?u.1862136
A : Type ?u.1862139
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ (∫ (y : ℝ) in a..b, f' y) = f b - f a
rw [← hderiv, integral_deriv_eq_sub hdiff]
ι : Type ?u.1862127
𝕜 : Type ?u.1862130
E : Type u_1
F : Type ?u.1862136
A : Type ?u.1862139
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ IntervalIntegrable f' volume a b
ι : Type ?u.1862127
𝕜 : Type ?u.1862130
E : Type u_1
F : Type ?u.1862136
A : Type ?u.1862139
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ IntervalIntegrable (deriv f) volume a b
rw [hderiv]
no goals
ι : Type ?u.1862127
𝕜 : Type ?u.1862130
E : Type u_1
F : Type ?u.1862136
A : Type ?u.1862139
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ IntervalIntegrable f' volume a b
exact hcont.intervalIntegrable