proposition: Lemma negligibleU 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: measurableU. - apply/eqP; rewrite -measure_le0 -N0 -[leRHS]adde0 -M0 -bigsetU_bigcup2. apply: le_trans. + apply: (@content_sub_additive _ _ _ _ _ (bigcup2 N M) 2%N) => //. * by move=> [|[|[|]]]. * apply: bigsetU_measurable => // i _; rewrite /bigcup2. by case: ifPn => // i0; case: ifPn. + by rewrite big_ord_recr/= big_ord_recr/= big_ord0 add0e. - exact: setUSS. 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)