ι : Type ?u.18470778
𝕜 : Type ?u.18470781
E : Type u_1
F : Type ?u.18470787
A : Type ?u.18470790
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntervalIntegrable f μ b₁ b₂
ha : a ∈ [[b₁, b₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[b₁, b₂]]
⊢ IntervalIntegrable (fun x => f x) μ (min a (b₁ ⊓ b₂)) (max a (b₁ ⊔ b₂))
ι : Type ?u.18470778
𝕜 : Type ?u.18470781
E : Type u_1
F : Type ?u.18470787
A : Type ?u.18470790
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntervalIntegrable f μ b₁ b₂
ha : a ∈ [[b₁, b₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[b₁, b₂]]
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) [[b₁, b₂]] x✝¹
refine continuousWithinAt_primitive (measure_singleton _) ?_
ι : Type ?u.18470778
𝕜 : Type ?u.18470781
E : Type u_1
F : Type ?u.18470787
A : Type ?u.18470790
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntervalIntegrable f μ b₁ b₂
ha : a ∈ [[b₁, b₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[b₁, b₂]]
⊢ IntervalIntegrable (fun x => f x) μ (b₁ ⊓ b₂) (b₁ ⊔ b₂)
ι : Type ?u.18470778
𝕜 : Type ?u.18470781
E : Type u_1
F : Type ?u.18470787
A : Type ?u.18470790
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntervalIntegrable f μ b₁ b₂
ha : a ∈ [[b₁, b₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[b₁, b₂]]
⊢ IntervalIntegrable (fun x => f x) μ (min a (b₁ ⊓ b₂)) (max a (b₁ ⊔ b₂))
rw [min_eq_right ha.1, max_eq_right ha.2]
no goals
ι : Type ?u.18470778
𝕜 : Type ?u.18470781
E : Type u_1
F : Type ?u.18470787
A : Type ?u.18470790
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntervalIntegrable f μ b₁ b₂
ha : a ∈ [[b₁, b₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[b₁, b₂]]
⊢ IntervalIntegrable (fun x => f x) μ (b₁ ⊓ b₂) (b₁ ⊔ b₂)
simpa [intervalIntegrable_iff, uIoc] using h_int