proposition: Lemma le_caratheodory_measurable (R : realType) T (mu : {outer_measure set T -> \bar R}) (A : set T) : (forall X, mu (X `&` A) + mu (X `&` ~` A) <= mu X) -> mu.-caratheodory A.
proof: Proof. move=> suf X; apply/eqP; rewrite eq_le; apply/andP; split; [exact: le_outer_measureIC | exact: suf]. 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)