proposition: Lemma caratheodory_measurable_setU_le (X A B : set T) : mu.-caratheodory A -> mu.-caratheodory B -> mu (X `&` (A `|` B)) + mu (X `&` ~` (A `|` B)) <= mu X.
proof: Proof. move=> mA mB; pose Y := X `&` A `|` X `&` B `&` ~` A. have /(leeD2r (mu (X `&` ~` (A `|` B)))) : mu Y <= mu (X `&` A) + mu (X `&` B `&` ~` A). pose Z := bigcup2 (X `&` A) (X `&` B `&` ~` A). have -> : Y = \bigcup_k Z k. rewrite predeqE => t; split=> [[?|?]|[]]; [by exists O|by exists 1%N|]. by move=> [_ ?|[_ ?|//]]; [left|right]. rewrite (le_trans (outer_measure_sigma_subadditive mu Z))//. rewrite le_eqVlt; apply/orP; left; apply/eqP. apply/cvg_lim => //; rewrite -(cvg_shiftn 2)/=; apply: cvg_near_cst. apply: nearW => k; rewrite big_mkord addn2 2!big_ord_recl big1 ?adde0//. by move=> ? _; exact: outer_measure0. have /le_trans : mu (X `&` (A `|` B)) + mu (X `&` ~` (A `|` B)) <= mu Y + mu (X `&` ~` (A `|` B)). rewrite setIUr (_ : X `&` A `|` X `&` B = Y) //. rewrite /Y -[in LHS](setIT B) -(setUCr A) 2!setIUr setUC -[in RHS]setIA. rewrite setUC setUA; congr (_ `|` _). by rewrite setUidPl setICA; apply: subIset; right. suff -> : mu (X `&` A) + mu (X `&` B `&` ~` A) + mu (X `&` (~` (A `|` B))) = mu X by exact. by rewrite setCU setIA -(setIA X) setICA (setIC B) -addeA -mB -mA. 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)