proposition: Lemma disjoint_caratheodoryIU X : [disjoint A & B] -> mu (X `&` (A `|` B)) = mu (X `&` A) + mu (X `&` B).
proof: Proof. move=> /eqP AB; rewrite caratheodory_decomp -setIA AB setI0 outer_measure0. rewrite add0e addeC -setIA -setCU -setIA setICr setI0 outer_measure0 add0e. rewrite -!setIA; congr (mu (X `&` _ ) + mu (X `&` _)). rewrite (setIC A) setIA setIC; apply/setIidPl. - by rewrite setIUl setICr setU0 subsetI; move/disjoints_subset in AB; split. - rewrite setIA setIC; apply/setIidPl; rewrite setIUl setICr set0U. by move: AB; rewrite setIC => /disjoints_subset => AB; rewrite subsetI; split. 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)