proposition: Lemma Hahn_decomposition_uniq P1 N1 P2 N2 : hahn_decomposition nu P1 N1 -> hahn_decomposition nu P2 N2 -> forall S, measurable S -> nu (S `&` P1) = nu (S `&` P2) /\ nu (S `&` N1) = nu (S `&` N2).
proof: Proof. move=> [psP1 nsN1 PN1T PN10] [psP2 nsN2 PN2T PN20] S mS. move: (psP1) (nsN1) (psP2) (nsN2) => [mP1 _] [mN1 _] [mP2 _] [mN2 _]. split. - transitivity (nu (S `&` P1 `&` P2)). + rewrite (charge_partition _ _ mP2 mN2)//; last exact: measurableI. by rewrite (positive_negative0 psP1 nsN2 mS) adde0. + rewrite [RHS](charge_partition _ _ mP1 mN1)//; last exact: measurableI. by rewrite (positive_negative0 psP2 nsN1 mS) adde0 setIAC. - transitivity (nu (S `&` N1 `&` N2)). + rewrite (charge_partition nu _ mP2 mN2)//; last exact: measurableI. have := positive_negative0 psP2 nsN1 mS. by rewrite setIAC => ->; rewrite add0e. + rewrite [RHS](charge_partition nu _ mP1 mN1)//; last exact: measurableI. by rewrite (setIAC _ _ P1) (positive_negative0 psP1 nsN2 mS) add0e setIAC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets cardinality) mathcomp(functions fsbigop set_interval) HB(structures) reals ereal signed topology numfun normedtype sequences esum measure realfun lebesgue_measure lebesgue_integral