proposition: Lemma measure_bigcup (D : set nat) F : (forall i, D i -> measurable (F i)) -> trivIset D F -> mu (\bigcup_(n in D) F n) = \sum_(i <oo | i \in D) mu (F i).
proof: Proof. move=> mF tF; rewrite bigcup_mkcond measure_semi_bigcup. - by rewrite [in RHS]eseries_mkcond; apply: eq_eseriesr => n _; case: ifPn. - by move=> i; case: ifPn => // /set_mem; exact: mF. - by move/trivIset_mkcond : tF. - by rewrite -bigcup_mkcond; apply: bigcup_measurable. 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)