proposition: Lemma measure_fsbig (I : choiceType) (A : set I) (F : I -> set T) : finite_set A -> (forall i, A i -> measurable (F i)) -> trivIset A F -> m (\big[setU/set0]_(i \in A) F i) = \sum_(i \in A) m (F i).
proof: Proof. move=> Afin Fm Ft. by rewrite fsbig_finite// -measure_fin_bigcup// -bigsetU_fset_set. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun