proposition: Lemma negligible_bigsetU (F : (set T)^nat) s (P : pred nat) : (forall k, P k -> mu.-negligible (F k)) -> mu.-negligible (\big[setU/set0]_(k <- s | P k) F k).
proof: Proof. by move=> PF; elim/big_ind : _ => //; [exact: negligible_set0|exact: negligibleU]. 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)