case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
a : α
s : Set β
⊢ MeasurableSet s → ↑↑(↑(kernel.sum fun x => 0) a) s = ↑↑(↑0 a) s
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
⊢ (kernel.sum fun x => 0) = 0
ext a s
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(kernel.sum fun x => 0) a) s = ↑↑(↑0 a) s
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
a : α
s : Set β
⊢ MeasurableSet s → ↑↑(↑(kernel.sum fun x => 0) a) s = ↑↑(↑0 a) s
intro hs
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
a : α
s : Set β
hs : MeasurableSet s
⊢ (∑' (n : ι), ↑↑(↑0 a) s) = ↑↑(↑0 a) s
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(kernel.sum fun x => 0) a) s = ↑↑(↑0 a) s
rw [sum_apply' _ a hs]
no goals
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
a : α
s : Set β
hs : MeasurableSet s
⊢ (∑' (n : ι), ↑↑(↑0 a) s) = ↑↑(↑0 a) s
simp only [zero_apply, Measure.coe_zero, Pi.zero_apply, tsum_zero]