proposition: Lemma Rmu_fin_bigcup (I : choiceType) (D : set I) (F : I -> set T) : finite_set D -> trivIset D F -> (forall i, i \in D -> measurable (F i)) -> Rmu (\bigcup_(i in D) F i) = \sum_(i \in D) mu (F i).
proof: Proof. move=> Dfin Ftriv Fm; rewrite /measure. have mUD : measurable (\bigcup_(i in D) F i : set rT). apply: fin_bigcup_measurable => // *; apply: sub_gen_smallest. exact/Fm/mem_set. have [->|/set0P[i0 Di0]] := eqVneq D set0. by rewrite bigcup_set0 decomp_set0 fsbig_set0 fsbig_set1. set E := decomp _; have Em X := decomp_measurable mUD X. transitivity (\sum_(X \in E) \sum_(i \in D) mu (X `&` F i)). apply: eq_fsbigr => /= X XE; have XDF : X = \bigcup_(i in D) (X `&` F i). by rewrite -setI_bigcupr setIidl//; exact: decomp_sub. rewrite [in LHS]XDF content_fin_bigcup//; first exact: trivIset_setIl. - by move=> i /mem_set Di; apply: measurableI; [exact: Em|exact: Fm]. - by rewrite -XDF; exact: Em. rewrite exchange_fsbig //; last exact: decomp_finite_set. apply: eq_fsbigr => i Di; have Feq : F i = \bigcup_(X in E) (X `&` F i). rewrite -setI_bigcupl setIidr// cover_decomp. by apply/bigcup_sup; exact: set_mem. rewrite -content_fin_bigcup -?Feq//; [exact/decomp_finite_set| | |exact/Fm]. - exact/trivIset_setIr/decomp_triv. - by move=> X /= XE; apply: measurableI; [apply: Em; rewrite inE | exact: Fm]. 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)