proposition: Lemma outer_measure_subadditive (F : nat -> set T) n : mu (\big[setU/set0]_(i < n) F i) <= \sum_(i < n) mu (F i).
proof: Proof. pose F' := fun k => if (k < n)%N then F k else set0. rewrite -(big_mkord xpredT F) big_nat (eq_bigr F')//; last first. by move=> k /= kn; rewrite /F' kn. rewrite -big_nat big_mkord. have := outer_measure_sigma_subadditive mu F'. rewrite (bigcup_splitn n) (_ : bigcup _ _ = set0) ?setU0; last first. by rewrite bigcup0 // => k _; rewrite /F' /= ltnNge leq_addr. move/le_trans; apply. rewrite (nneseries_split n); last by move=> ?; exact: outer_measure_ge0. rewrite [X in _ + X](_ : _ = 0) ?adde0//; last first. rewrite eseries_cond/= eseries_mkcond eseries0//. by move=> k _; case: ifPn => //; rewrite /F' leqNgt => /negbTE ->. by apply: lee_sum => i _; rewrite /F' ltn_ord. 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)