fact: Definition sigma_algebra := [/\ G set0, (forall A, G A -> G (D `\` A)) & (forall A : (set T)^nat, (forall n, G (A n)) -> G (\bigcup_k A k))].
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)