proposition: Lemma fin_bigcup_measurable I (D : set I) (F : I -> set T) : finite_set D -> (forall i, D i -> measurable (F i)) -> measurable (\bigcup_(i in D) F i).
proof: Proof. elim/Pchoice: I => I in D F * => Dfin Fm. rewrite -bigsetU_fset_set// big_seq; apply: bigsetU_measurable => i. by rewrite in_fset_set ?inE// => *; apply: 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)