proposition: Lemma measure_semi_additive_ord (n : nat) (F : 'I_n -> set T) : (forall (k : 'I_n), measurable (F k)) -> trivIset setT F -> measurable (\big[setU/set0]_(k < n) F k) -> mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i).
proof: Proof. move=> mF tF mUF; pose F' (i : nat) := oapp F set0 (insub i). have FE (i : 'I_n) : F i = (F' \o val) i by rewrite /F'/= valK/=. rewrite (eq_bigr (F' \o val))// (eq_bigr (mu \o F' \o val))//; last first. by move=> i _; rewrite FE. rewrite -measure_semi_additive//. - by move=> k; rewrite /F'; case: insubP => /=. - apply/trivIsetP=> i j _ _; rewrite /F'. do 2?[case: insubP; rewrite ?(set0I, setI0)//= => ? _ <-]. by move/trivIsetP: tF; apply. - by rewrite (eq_bigr (F' \o val)) in mUF. 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)