proposition: Lemma content_fin_bigcup (I : choiceType) (D : set I) (F : I -> set T) : finite_set D -> trivIset D F -> (forall i, D i -> measurable (F i)) -> measurable (\bigcup_(i in D) F i) -> mu (\bigcup_(i in D) F i) = \sum_(i \in D) mu (F i).
proof: Proof. elim/choicePpointed: I => I in D F *. by rewrite !emptyE => *; rewrite fsbig_set0 bigcup0. move=> [n /ppcard_eqP[f]] Ftriv Fm UFm. rewrite -(image_eq [surjfun of f^-1%FUN])/= in UFm Ftriv *. rewrite bigcup_image fsbig_image//= bigcup_mkord -fsbig_ord/= in UFm *. rewrite (@measure_semi_additive_ord_I (F \o f^-1))//= 1?trivIset_comp//. by move=> k kn; apply: Fm; exact: funS. 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)