proposition: Lemma measureUfinr A B : measurable A -> measurable B -> mu B < +oo -> mu (A `|` B) = mu A + mu B - mu (A `&` B).
proof: Proof. move=> Am Bm mBfin; rewrite -[B in LHS](setDUK (@subIsetl _ _ A)) setUA. rewrite [A `|` _]setUidl; last exact: subIsetr. rewrite measureU//=; [|rewrite setDIr setDv set0U ?setDIK//..]. - by rewrite measureD// ?setIA ?setIid 1?setIC ?addeA//; exact: measurableI. - exact: measurableD. 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)