ι : Type ?u.12763718
𝕜 : Type ?u.12763721
E : Type u_1
F : Type ?u.12763727
A : Type ?u.12763730
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
⊢ ((-∫ (a : ℝ) in Ioc a b, f a ∂μ) - -∫ (a : ℝ) in Ioc b a, f a ∂μ) =
    -((∫ (a : ℝ) in Ioc a b, f a ∂μ) - ∫ (a : ℝ) in Ioc b a, f a ∂μ)
ι : Type ?u.12763718
𝕜 : Type ?u.12763721
E : Type u_1
F : Type ?u.12763727
A : Type ?u.12763730
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
⊢ (∫ (x : ℝ) in a..b, -f x ∂μ) = -∫ (x : ℝ) in a..b, f x ∂μ
simp only [intervalIntegral, integral_neg]
no goals
ι : Type ?u.12763718
𝕜 : Type ?u.12763721
E : Type u_1
F : Type ?u.12763727
A : Type ?u.12763730
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
⊢ ((-∫ (a : ℝ) in Ioc a b, f a ∂μ) - -∫ (a : ℝ) in Ioc b a, f a ∂μ) =
    -((∫ (a : ℝ) in Ioc a b, f a ∂μ) - ∫ (a : ℝ) in Ioc b a, f a ∂μ)
abel