proposition: Lemma dynkin_setI_bigsetI G (F : (set T)^nat) : dynkin G -> setI_closed G -> (forall n, G (F n)) -> forall n, G (\big[setI/setT]_(i < n) F i).
proof: Proof. move=> dG GI GF; elim => [|n ih]; last by rewrite big_ord_recr /=; apply: GI. by rewrite big_ord0; exact: (dynkinT dG). 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)