proposition: Lemma monotone_class_g_salgebra T (G : set (set T)) (D : set T) : (forall X, <<s D, G >> X -> X `<=` D) -> G D -> monotone_class D (<<s D, G >>).
proof: Proof. move=> sDGD GD; have := smallest_sigma_algebra D G. by move=> /(sigma_algebraP sDGD) [sT sD snd sI]; split. 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)