proposition: Lemma sigma_algebra_bigcap T (I : choiceType) (D : set T) (F : I -> set (set T)) (J : set I) : (forall n, J n -> sigma_algebra D (F n)) -> sigma_algebra D (\bigcap_(i in J) F i).
proof: Proof. move=> mG; split=> [i Ji|A AJ i Ji|H GH i Ji]; first by have [] := mG i. - by have [_ mGiC _] := mG i Ji; exact/mGiC/AJ. - by have [_ _ mGiU] := mG i Ji; apply: mGiU => j; exact: GH. 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)