proposition: Lemma le_outer_measureIC (R : realFieldType) T (mu : {outer_measure set T -> \bar R}) (A X : set T) : mu X <= mu (X `&` A) + mu (X `&` ~` A).
proof: Proof. pose B : (set T) ^nat := bigcup2 (X `&` A) (X `&` ~` A). have cvg_mu : (fun n => \sum_(i < n) mu (B i)) @ \oo --> mu (B 0%N) + mu (B 1%N). rewrite -2!cvg_shiftS /=. rewrite [X in X @ \oo --> _](_ : _ = (fun=> mu (B 0%N) + mu (B 1%N))); last first. rewrite funeqE => i; rewrite 2!big_ord_recl /= big1 ?adde0 // => j _. by rewrite /B /bigcup2 /=. exact: cvg_cst. have := outer_measure_sigma_subadditive mu B. suff : \bigcup_n B n = X. move=> -> /le_trans; apply; under eq_fun do rewrite big_mkord. by rewrite (cvg_lim _ cvg_mu). transitivity (\big[setU/set0]_(i < 2) B i). by rewrite (bigcup_splitn 2) // -bigcup_mkord setUidl// => t -[]. by rewrite 2!big_ord_recl big_ord0 setU0 /= -setIUr setUCr setIT. Unshelve. all: by end_near. 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)