proposition: Lemma bigsetI_measurable I r (P : pred I) (F : I -> set T) : (forall i, P i -> measurable (F i)) -> measurable (\big[setI/setT]_(i <- r | P i) F i).
proof: Proof. move=> mF; rewrite -[X in measurable X]setCK setC_bigsetI; apply: measurableC. by apply: bigsetU_measurable => i Pi; apply/measurableC/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)