proposition: Lemma smallest_sigma_algebra : sigma_algebra D <<s D, G >>.
proof: Proof. split=> [|A GA|A GA] P [[P0 PD PU]] GP //. by apply: (PD); apply: GA. by apply: (PU) => n; apply: GA. 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)