proposition: Lemma caratheodory_measurable_bigsetU (A : (set T) ^nat) : (forall n, M (A n)) -> forall n, M (\big[setU/set0]_(i < n) A i).
proof: Proof. move=> MA n; elim/big_ind : _ => //; first exact: caratheodory_measurable_set0. exact: caratheodory_measurable_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)