α : Type u_2
β : Type ?u.2919204
γ : Type ?u.2919207
γ₂ : Type ?u.2919210
δ : Type ?u.2919213
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x => ⨆ (s : Finset ι), ∑ i in s, f i x
α : Type u_2
β : Type ?u.2919204
γ : Type ?u.2919207
γ₂ : Type ?u.2919210
δ : Type ?u.2919213
ι✝ : 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 [ENNReal.tsum_eq_iSup_sum]
case hf
α : Type u_2
β : Type ?u.2919204
γ : Type ?u.2919207
γ₂ : Type ?u.2919210
δ : Type ?u.2919213
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ ∀ (i : Finset ι), Measurable fun b => ∑ i in i, f i b
α : Type u_2
β : Type ?u.2919204
γ : Type ?u.2919207
γ₂ : Type ?u.2919210
δ : Type ?u.2919213
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x => ⨆ (s : Finset ι), ∑ i in s, f i x
apply measurable_iSup
no goals
case hf
α : Type u_2
β : Type ?u.2919204
γ : Type ?u.2919207
γ₂ : Type ?u.2919210
δ : Type ?u.2919213
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ ∀ (i : Finset ι), Measurable fun b => ∑ i in i, f i b
exact fun s => s.measurable_sum fun i _ => h i