proposition: Lemma caratheodory_measurable_bigcup (A : (set T) ^nat) : (forall n, M (A n)) -> M (\bigcup_k (A k)).
proof: Proof. move=> MA; rewrite -eq_bigcup_seqD_bigsetU. apply/caratheodory_measurable_trivIset_bigcup; last first. by apply: trivIset_seqD => m n mn; exact/subsetPset/subset_bigsetU. by case=> [|n /=]; [| apply/caratheodory_measurable_setD => //]; exact/caratheodory_measurable_bigsetU. 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)