case h
α : Type u_1
β : Type ?u.16597
inst✝ : MeasurableSpace α
j : JordanDecomposition α
i : Set α
hi : MeasurableSet i
⊢ ↑(toSignedMeasure 0) i = ↑0 i
α : Type u_1
β : Type ?u.16597
inst✝ : MeasurableSpace α
j : JordanDecomposition α
⊢ toSignedMeasure 0 = 0
ext1 i hi
no goals
case h
α : Type u_1
β : Type ?u.16597
inst✝ : MeasurableSpace α
j : JordanDecomposition α
i : Set α
hi : MeasurableSet i
⊢ ↑(toSignedMeasure 0) i = ↑0 i
rw [toSignedMeasure, toSignedMeasure_sub_apply hi, zero_posPart, zero_negPart, sub_self,
  VectorMeasure.coe_zero, Pi.zero_apply]