proposition: Lemma outer_measureU2 A B : mu (A `|` B) <= mu A + mu B.
proof: Proof. have := outer_measure_subadditive (bigcup2 A B) 2. by rewrite !big_ord_recl/= !big_ord0 setU0 adde0. 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)