ι : Type ?u.18752176
𝕜 : Type ?u.18752179
E : Type u_1
F : Type ?u.18752185
A : Type ?u.18752188
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f [[b, a]]
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in x..b, f t ∂μ) [[b, a]]
ι : Type ?u.18752176
𝕜 : Type ?u.18752179
E : Type u_1
F : Type ?u.18752185
A : Type ?u.18752188
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f [[a, b]]
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in x..b, f t ∂μ) [[a, b]]
rw [uIcc_comm a b] at h_int ⊢
ι : Type ?u.18752176
𝕜 : Type ?u.18752179
E : Type u_1
F : Type ?u.18752185
A : Type ?u.18752188
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f [[b, a]]
⊢ ContinuousOn (fun x => -∫ (x : ℝ) in b..x, f x ∂μ) [[b, a]]
ι : Type ?u.18752176
𝕜 : Type ?u.18752179
E : Type u_1
F : Type ?u.18752185
A : Type ?u.18752188
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f [[b, a]]
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in x..b, f t ∂μ) [[b, a]]
simp only [integral_symm b]
no goals
ι : Type ?u.18752176
𝕜 : Type ?u.18752179
E : Type u_1
F : Type ?u.18752185
A : Type ?u.18752188
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f [[b, a]]
⊢ ContinuousOn (fun x => -∫ (x : ℝ) in b..x, f x ∂μ) [[b, a]]
exact (continuousOn_primitive_interval h_int).neg