proposition: Theorem Boole_inequality (A : (set T) ^nat) n : (forall i, (i < n)%N -> measurable (A i)) -> mu (\big[setU/set0]_(i < n) A i) <= \sum_(i < n) mu (A i).
proof: Proof. move=> Am; rewrite content_sub_additive// -bigcup_mkord. exact: fin_bigcup_measurable. 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)