proposition: Lemma measure_fbigsetU (I : choiceType) (A : {fset I}) (F : I -> set T) : (forall i, i \in A -> measurable (F i)) -> trivIset [set` A] F -> mu (\big[setU/set0]_(i <- A) F i) = (\sum_(i <- A) mu (F i))%E.
proof: Proof. by move=> mF tF; rewrite -bigcup_fset measure_fin_bigcup// -fsbig_seq. 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)