proposition: Lemma measure_bigsetU_ord_cond n (P : {pred 'I_n}) (F : 'I_n -> set T) : (forall i : 'I_n, P i -> measurable (F i)) -> trivIset P F -> mu (\big[setU/set0]_(i < n | P i) F i) = (\sum_(i < n | P i) mu (F i))%E.
proof: Proof. move=> mF tF; rewrite !(big_mkcond P)/= measure_semi_additive_ord//. - by apply: eq_bigr => i _; rewrite (fun_if mu) measure0. - by move=> k; case: ifP => //; apply: mF. - by rewrite -patch_pred trivIset_restr setIT. - by apply: bigsetU_measurable=> k _; case: ifP => //; apply: mF. 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)