proposition: Lemma negligible_bigcup d (T : measurableType d) (R : realFieldType) (mu : {measure set T -> \bar R}) (F : (set T)^nat) : (forall k, mu.-negligible (F k)) -> mu.-negligible (\bigcup_k F k).
proof: Proof. move=> mF; exists (\bigcup_k sval (cid (mF k))); split. - by apply: bigcupT_measurable => // k; have [] := svalP (cid (mF k)). - rewrite seqDU_bigcup_eq measure_bigcup//; last first. move=> k _; apply: measurableD; first by case: cid => //= A []. by apply: bigsetU_measurable => i _; case: cid => //= A []. rewrite eseries0// => k _. have [mFk mFk0 ?] := svalP (cid (mF k)). rewrite measureD//=. + rewrite mFk0 sub0e eqe_oppLRP oppe0; apply/eqP; rewrite -measure_le0. rewrite -[leRHS]mFk0 le_measure//= ?inE//; apply: measurableI => //. by apply: bigsetU_measurable => i _; case: cid => // A []. + by apply: bigsetU_measurable => i _; case: cid => // A []. + by rewrite mFk0. - by apply: subset_bigcup => k _; rewrite /sval/=; by case: cid => //= A []. 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)