proposition: Lemma caratheodory_measure_sigma_additive : semi_sigma_additive (mu : set U -> _).
proof: Proof. move=> A mA tA mbigcupA; set B := \bigcup_k A k. suff : forall X, mu X = \sum_(k <oo) mu (X `&` A k) + mu (X `&` ~` B). move/(_ B); rewrite setICr outer_measure0 adde0. rewrite (_ : (fun n => _) = fun n => \sum_(k < n) mu (A k)); last first. rewrite funeqE => n; rewrite big_mkord; apply: eq_bigr => i _; congr (mu _). by rewrite setIC; apply/setIidPl; exact: bigcup_sup. move=> ->; have := fun n (_ : xpredT n) => outer_measure_ge0 mu (A n). move/(@is_cvg_nneseries _ _ _ 0) => /cvg_ex[l] hl. under [in X in _ --> X]eq_fun do rewrite -(big_mkord xpredT (mu \o A)). by move/cvg_lim : (hl) => ->. move=> X. have mB : mu.-cara.-measurable B := caratheodory_measurable_bigcup mA. apply/eqP; rewrite eq_le (caratheodory_lime_le mA tA X) andbT. have /(leeD2r (mu (X `&` ~` B))) := outer_measure_bigcup_lim mu A X. by rewrite -le_caratheodory_measurable // => ?; rewrite -mB. 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)