proposition: Lemma outer_measure_bigcup_lim (A : (set T) ^nat) X : mu (X `&` \bigcup_k A k) <= \sum_(k <oo) mu (X `&` A k).
proof: Proof. apply: (le_trans _ (outer_measure_sigma_subadditive mu (fun n => X `&` A n))). by apply/le_outer_measure; rewrite setI_bigcupr. 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)