proposition: Lemma dynkin_g_dynkin G : dynkin (<<d G >>).
proof: Proof. split=> [D /= [] []//| | ]. - by move=> Y sGY D /= [dD GD]; exact/(dynkinC dD)/(sGY D). - by move=> F tF gGF D /= [dD GD]; apply dD => // k; exact: gGF. 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)