proposition: Lemma dynkin_setI_sigma_algebra G : dynkin G -> setI_closed G -> sigma_algebra setT G.
proof: Proof. move=> dG GI; split => [|//|F DF]. - by rewrite -setCT; exact/(dynkinC dG)/(dynkinT dG). - by move=> A GA; rewrite setTD; exact: (dynkinC dG). - rewrite seqDU_bigcup_eq; apply/(dynkinU dG) => //. move=> n; rewrite /seqDU setDE; apply GI => //. rewrite -bigcup_mkord setC_bigcup bigcap_mkord. by apply: (@dynkin_setI_bigsetI _ (fun x => ~` F x)) => // ?; exact/(dynkinC 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)