proposition: Lemma bigcap_measurable F P : (forall k, P k -> measurable (F k)) -> measurable (\bigcap_(i in P) F i).
proof: Proof. move=> PF; rewrite -[X in measurable X]setCK setC_bigcap; apply: measurableC. by apply: bigcup_measurable => k Pk; exact/measurableC/PF. 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)