ι : Type ?u.10756409
𝕜 : Type ?u.10756412
E : Type u_1
F : Type ?u.10756418
A : Type ?u.10756421
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
f : ℝ → E
a b : ℝ
⊢ ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ) ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
ι : Type ?u.10756409
𝕜 : Type ?u.10756412
E : Type u_1
F : Type ?u.10756418
A : Type ?u.10756421
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
f : ℝ → E
a b : ℝ
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
rw [intervalIntegral_eq_integral_uIoc]
no goals
ι : Type ?u.10756409
𝕜 : Type ?u.10756412
E : Type u_1
F : Type ?u.10756418
A : Type ?u.10756421
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
f : ℝ → E
a b : ℝ
⊢ ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ) ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
split_ifs <;> simp