proposition: Lemma caratheodory_additive (A : (set T) ^nat) : (forall n, M (A n)) -> trivIset setT A -> forall n X, mu (X `&` \big[setU/set0]_(i < n) A i) = \sum_(i < n) mu (X `&` A i).
proof: Proof. move=> MA ta; elim=> [|n ih] X; first by rewrite !big_ord0 setI0 outer_measure0. rewrite big_ord_recr /= disjoint_caratheodoryIU // ?ih ?big_ord_recr //. - exact: caratheodory_measurable_bigsetU. - by apply/eqP/(@trivIset_bigsetUI _ predT) => //; rewrite /predT /= trueE. 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)