proposition: Lemma measureDI A B : measurable A -> measurable B -> mu A = mu (A `\` B) + mu (A `&` B).
proof: Proof. move=> mA mB; rewrite -measure_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 all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)