case h.e'_5.h
α : Type u_2
β : Type ?u.2920454
γ : Type ?u.2920457
γ₂ : Type ?u.2920460
δ : Type ?u.2920463
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
x : α
⊢ tsum (fun i => f i) x = ∑' (i : ι), f i x
α : Type u_2
β : Type ?u.2920454
γ : Type ?u.2920457
γ₂ : Type ?u.2920460
δ : Type ?u.2920463
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable (∑' (i : ι), f i)
convert Measurable.ennreal_tsum h with x
no goals
case h.e'_5.h
α : Type u_2
β : Type ?u.2920454
γ : Type ?u.2920457
γ₂ : Type ?u.2920460
δ : Type ?u.2920463
ι✝ : Sort y
s t u : Set α
inst✝¹ : MeasurableSpace α
ι : Type u_1
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
x : α
⊢ tsum (fun i => f i) x = ∑' (i : ι), f i x
exact tsum_apply (Pi.summable.2 fun _ => ENNReal.summable)