case h.e'_3.h
α : Type u_2
ι : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f
h : Tendsto (fun i => ∫ (x : α), indicator (φ i) f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
x✝ : ι
⊢ (∫ (x : α) in φ x✝, f x ∂μ) = ∫ (x : α), indicator (φ x✝) f x ∂μ
α : Type u_2
ι : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f
h : Tendsto (fun i => ∫ (x : α), indicator (φ i) f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
⊢ Tendsto (fun i => ∫ (x : α) in φ i, f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
convert h using 2
no goals
case h.e'_3.h
α : Type u_2
ι : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f
h : Tendsto (fun i => ∫ (x : α), indicator (φ i) f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
x✝ : ι
⊢ (∫ (x : α) in φ x✝, f x ∂μ) = ∫ (x : α), indicator (φ x✝) f x ∂μ
rw [integral_indicator (hφ.measurableSet _)]