α : Type u_2
ι : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) ≤ ENNReal.ofReal I
⊢ Tendsto (fun c => ∫⁻ (x : α) in φ c, ↑‖f x‖₊ ∂μ) l (𝓝 (∫⁻ (a : α), ↑‖f a‖₊ ∂μ))
α : Type u_2
ι : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) ≤ ENNReal.ofReal I
⊢ Integrable f
refine' ⟨hfm, (le_of_tendsto _ hbounded).trans_lt ENNReal.ofReal_lt_top⟩
no goals
α : Type u_2
ι : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) ≤ ENNReal.ofReal I
⊢ Tendsto (fun c => ∫⁻ (x : α) in φ c, ↑‖f x‖₊ ∂μ) l (𝓝 (∫⁻ (a : α), ↑‖f a‖₊ ∂μ))
exact hφ.lintegral_tendsto_of_countably_generated hfm.ennnorm