proposition: Lemma caratheodory_measurable_trivIset_bigcup (A : (set T) ^nat) : (forall n, M (A n)) -> trivIset setT A -> M (\bigcup_k (A k)).
proof: Proof. move=> MA tA; apply: le_caratheodory_measurable => X /=. have /(leeD2r (mu (X `&` ~` \bigcup_k A k))) := outer_measure_bigcup_lim A X. by move/le_trans; apply; exact: caratheodory_lime_le. 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)