case a
α : Type u_1
β : Type ?u.74331
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ toSignedMeasure (toJordanDecomposition (-s)) = toSignedMeasure (-toJordanDecomposition s)
α : Type u_1
β : Type ?u.74331
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ toJordanDecomposition (-s) = -toJordanDecomposition s
apply toSignedMeasure_injective
no goals
case a
α : Type u_1
β : Type ?u.74331
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ toSignedMeasure (toJordanDecomposition (-s)) = toSignedMeasure (-toJordanDecomposition s)
simp [toSignedMeasure_neg]