proposition: Lemma charge_partition nu S P N : measurable S -> measurable P -> measurable N -> P `|` N = [set: T] -> P `&` N = set0 -> nu S = nu (S `&` P) + nu (S `&` N).
proof: Proof. move=> mS mP mN PNT PN0; rewrite -{1}(setIT S) -PNT setIUr chargeU//. - exact: measurableI. - exact: measurableI. - by rewrite setICA -(setIA S P N) PN0 setIA setI0. 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