proposition: Lemma caratheodory_lime_le (A : (set T) ^nat) : (forall n, M (A n)) -> trivIset setT A -> forall X, \sum_(k <oo) mu (X `&` A k) + mu (X `&` ~` \bigcup_k A k) <= mu X.
proof: Proof. move=> MA tA X. set A' := \bigcup_k A k; set B := fun n => \big[setU/set0]_(k < n) (A k). suff : forall n, \sum_(k < n) mu (X `&` A k) + mu (X `&` ~` A') <= mu X. move=> XA; rewrite (_ : limn _ = ereal_sup ((fun n => \sum_(k < n) mu (X `&` A k)) @` setT)); last first. under eq_fun do rewrite big_mkord. apply/cvg_lim => //; apply: ereal_nondecreasing_cvgn. apply: (lee_sum_nneg_ord (fun n => mu (X `&` A n)) xpredT) => n _. exact: outer_measure_ge0. move XAx : (mu (X `&` ~` A')) => [x| |]. - rewrite -lee_subr_addr //; apply: ub_ereal_sup => /= _ [n _] <-. by rewrite EFinN lee_subr_addr // -XAx XA. - suff : mu X = +oo by move=> ->; rewrite leey. by apply/eqP; rewrite -leye_eq -XAx le_outer_measure. - by rewrite addeNy leNye. move=> n. apply: (@le_trans _ _ (\sum_(k < n) mu (X `&` A k) + mu (X `&` ~` B n))). apply/leeD2l/le_outer_measure; apply: setIS; exact/subsetC/bigsetU_bigcup. rewrite [in leRHS](caratheodory_measurable_bigsetU MA n) leeD2r//. by rewrite caratheodory_additive. 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)