proposition: Lemma measure_fin_bigcup (I : choiceType) (D : set I) (F : I -> set T) : finite_set D -> trivIset D F -> (forall i, D i -> measurable (F i)) -> mu (\bigcup_(i in D) F i) = \sum_(i \in D) mu (F i).
proof: Proof. move=> Dfin Ftriv Fm; rewrite content_fin_bigcup//. exact: fin_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)