no goals
ι : Type u_2
𝕜 : Type ?u.377817
E : Type u_1
F : Type ?u.377823
A : Type ?u.377826
inst✝⁴ : NormedAddCommGroup E
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
c ca cb : E
l l' la la' lb lb' : Filter ℝ
lt : Filter ι
μ : MeasureTheory.Measure ℝ
u v ua va ub vb : ι → ℝ
inst✝¹ : IsMeasurablyGenerated l'
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l'
hf : Tendsto f (l' ⊓ Measure.ae μ) (𝓝 c)
hl : Measure.FiniteAtFilter μ l'
hu : Tendsto u lt l
hv : Tendsto v lt l
huv : u ≤ᶠ[lt] v
x : ι
hx : u x ≤ v x
⊢ (fun t => (∫ (x : ℝ) in u t..v t, f x ∂μ) - ∫ (x : ℝ) in u t..v t, c ∂μ) x =
    (fun t => (∫ (x : ℝ) in u t..v t, f x ∂μ) - ENNReal.toReal (↑↑μ (Ioc (u t) (v t))) • c) x
simp [integral_const', hx]
no goals
ι : Type u_2
𝕜 : Type ?u.377817
E : Type u_1
F : Type ?u.377823
A : Type ?u.377826
inst✝⁴ : NormedAddCommGroup E
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
c ca cb : E
l l' la la' lb lb' : Filter ℝ
lt : Filter ι
μ : MeasureTheory.Measure ℝ
u v ua va ub vb : ι → ℝ
inst✝¹ : IsMeasurablyGenerated l'
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l'
hf : Tendsto f (l' ⊓ Measure.ae μ) (𝓝 c)
hl : Measure.FiniteAtFilter μ l'
hu : Tendsto u lt l
hv : Tendsto v lt l
huv : u ≤ᶠ[lt] v
x : ι
hx : u x ≤ v x
⊢ (fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ) x = (fun t => ENNReal.toReal (↑↑μ (Ioc (u t) (v t)))) x
simp [integral_const', hx]