proposition: Lemma chargeDI nu (A B : set T) : measurable A -> measurable B -> nu A = nu (A `\` B) + nu (A `&` B).
proof: Proof. move=> mA mB; rewrite -charge_semi_additive2. - by rewrite -setDDr setDv setD0. - exact: measurableD. - exact: measurableI. - by apply: measurableU; [exact: measurableD |exact: measurableI]. - by rewrite setDE setIACA setICl 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