case h
α : Type u_1
β : Type ?u.135956
m : MeasurableSpace α
i : Set α
⊢ MeasurableSet i → ↑(toSignedMeasure 0) i = ↑0 i
α : Type u_1
β : Type ?u.135956
m : MeasurableSpace α
⊢ toSignedMeasure 0 = 0
ext i
no goals
case h
α : Type u_1
β : Type ?u.135956
m : MeasurableSpace α
i : Set α
⊢ MeasurableSet i → ↑(toSignedMeasure 0) i = ↑0 i
simp