α : Type u_2
β : Type ?u.2930876
γ : Type ?u.2930879
γ₂ : Type ?u.2930882
δ : Type ?u.2930885
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
μ : MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable (f i)
⊢ AEMeasurable fun x => ⨆ (s : Finset ι), ∑ i in s, f i x
α : Type u_2
β : Type ?u.2930876
γ : Type ?u.2930879
γ₂ : Type ?u.2930882
δ : Type ?u.2930885
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
μ : MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable (f i)
⊢ AEMeasurable fun x => ∑' (i : ι), f i x
simp_rw [ENNReal.tsum_eq_iSup_sum]
case hf
α : Type u_2
β : Type ?u.2930876
γ : Type ?u.2930879
γ₂ : Type ?u.2930882
δ : Type ?u.2930885
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
μ : MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable (f i)
⊢ ∀ (i : Finset ι), AEMeasurable fun b => ∑ i in i, f i b
α : Type u_2
β : Type ?u.2930876
γ : Type ?u.2930879
γ₂ : Type ?u.2930882
δ : Type ?u.2930885
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
μ : MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable (f i)
⊢ AEMeasurable fun x => ⨆ (s : Finset ι), ∑ i in s, f i x
apply aemeasurable_iSup
no goals
case hf
α : Type u_2
β : Type ?u.2930876
γ : Type ?u.2930879
γ₂ : Type ?u.2930882
δ : Type ?u.2930885
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
μ : MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable (f i)
⊢ ∀ (i : Finset ι), AEMeasurable fun b => ∑ i in i, f i b
exact fun s => Finset.aemeasurable_sum s fun i _ => h i