α : Type u_2
β : Type ?u.2930312
γ : Type ?u.2930315
γ₂ : Type ?u.2930318
δ : Type ?u.2930321
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x => ENNReal.toNNReal (∑' (b : ι), ↑(f b x))
α : Type u_2
β : Type ?u.2930312
γ : Type ?u.2930315
γ₂ : Type ?u.2930318
δ : Type ?u.2930321
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x => ∑' (i : ι), f i x
simp_rw [NNReal.tsum_eq_toNNReal_tsum]
no goals
α : Type u_2
β : Type ?u.2930312
γ : Type ?u.2930315
γ₂ : Type ?u.2930318
δ : Type ?u.2930321
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x => ENNReal.toNNReal (∑' (b : ι), ↑(f b x))
exact (Measurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal