proposition: Lemma content_sub_fsum (I : choiceType) D (A : set T) (A_ : I -> set T) : finite_set D -> (forall i, D i -> measurable (A_ i)) -> measurable A -> A `<=` \bigcup_(i in D) A_ i -> mu A <= \sum_(i \in D) mu (A_ i).
proof: Proof. elim/choicePpointed: I => I in A_ D *. rewrite !emptyE bigcup_set0// subset0 => _ _ _ ->. by rewrite measure0 fsbig_set0. move=> Dfin A_m Am Asub; have [n /ppcard_eqP[f]] := Dfin. rewrite (reindex_fsbig f^-1%FUN `I_n)//= -fsbig_ord. rewrite (@content_sub_additive A (A_ \o f^-1%FUN))//=. by move=> i ltin; apply: A_m; apply: funS. rewrite (fsbig_ord _ _ (A_ \o f^-1%FUN))/= -(reindex_fsbig _ _ D)//=. by rewrite fsbig_setU. 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)