α✝ : Type ?u.2984900
β : Type ?u.2984903
γ : Type ?u.2984906
γ₂ : Type ?u.2984909
δ : Type ?u.2984912
ι✝ : Sort y
s t u : Set α✝
inst✝² : MeasurableSpace α✝
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0
μ : MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable (f i)
⊢ AEMeasurable fun x => ENNReal.toNNReal (∑' (b : ι), ↑(f b x))
α✝ : Type ?u.2984900
β : Type ?u.2984903
γ : Type ?u.2984906
γ₂ : Type ?u.2984909
δ : Type ?u.2984912
ι✝ : Sort y
s t u : Set α✝
inst✝² : MeasurableSpace α✝
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0
μ : MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable (f i)
⊢ AEMeasurable fun x => ∑' (i : ι), f i x
simp_rw [NNReal.tsum_eq_toNNReal_tsum]
no goals
α✝ : Type ?u.2984900
β : Type ?u.2984903
γ : Type ?u.2984906
γ₂ : Type ?u.2984909
δ : Type ?u.2984912
ι✝ : Sort y
s t u : Set α✝
inst✝² : MeasurableSpace α✝
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0
μ : MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable (f i)
⊢ AEMeasurable fun x => ENNReal.toNNReal (∑' (b : ι), ↑(f b x))
exact (AEMeasurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal