proposition: Lemma measure_is_complete_caratheodory : measure_is_complete (mu : set (caratheodory_type mu) -> _).
proof: Proof. move=> B [A [mA muA0 BA]]; apply: le_caratheodory_measurable => X. suff -> : mu (X `&` B) = 0. by rewrite add0e le_outer_measure //; apply: subIset; left. have muB0 : mu B = 0. apply/eqP; rewrite eq_le outer_measure_ge0 andbT. by apply: (le_trans (le_outer_measure mu _ _ BA)); rewrite -muA0. apply/eqP; rewrite eq_le outer_measure_ge0 andbT. have : X `&` B `<=` B by apply: subIset; right. by move/(le_outer_measure mu); rewrite muB0 => ->. 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)