ι : Type ?u.16319140
𝕜 : Type ?u.16319143
E : Type u_1
F : Type ?u.16319149
A : Type ?u.16319152
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c✝ d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : IsFiniteMeasure μ
c : E
⊢ (∫ (x : ℝ) in a..b, c ∂μ) = (∫ (x : ℝ) in Iic b, c ∂μ) - ∫ (x : ℝ) in Iic a, c ∂μ
ι : Type ?u.16319140
𝕜 : Type ?u.16319143
E : Type u_1
F : Type ?u.16319149
A : Type ?u.16319152
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c✝ d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : IsFiniteMeasure μ
c : E
⊢ (∫ (x : ℝ) in a..b, c ∂μ) = (ENNReal.toReal (↑↑μ (Iic b)) - ENNReal.toReal (↑↑μ (Iic a))) • c
simp only [sub_smul, ← set_integral_const]
no goals
ι : Type ?u.16319140
𝕜 : Type ?u.16319143
E : Type u_1
F : Type ?u.16319149
A : Type ?u.16319152
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c✝ d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : IsFiniteMeasure μ
c : E
⊢ (∫ (x : ℝ) in a..b, c ∂μ) = (∫ (x : ℝ) in Iic b, c ∂μ) - ∫ (x : ℝ) in Iic a, c ∂μ
refine' (integral_Iic_sub_Iic _ _).symm <;>
  simp only [integrableOn_const, measure_lt_top, or_true_iff]