proposition: Lemma negligibleI A B : mu.-negligible A -> mu.-negligible B -> mu.-negligible (A `&` B).
proof: Proof. move=> [N [mN N0 AN]] [M [mM M0 BM]]; exists (N `&` M); split => //. - exact: measurableI. - by apply/eqP; rewrite -measure_le0 -N0 le_measure ?inE//; exact: measurableI. - exact: setISS. 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)