proposition: Lemma sigma_algebra_dynkin G : sigma_algebra setT G -> dynkin G.
proof: Proof. case=> ? DC DU; split => [| |? ? ?]; last exact: DU. - by rewrite -setC0 -setTD; exact: DC. - by move=> A GA; rewrite -setTD; apply: DC. 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)