proposition: Lemma semi_sigma_additiveE (R : numFieldType) d (T : measurableType d) (mu : set T -> \bar R) : semi_sigma_additive mu = sigma_additive mu.
proof: Proof. rewrite propeqE; split=> [amu A mA tA|amu A mA tA mbigcupA]; last exact: amu. by apply: amu => //; exact: bigcupT_measurable. 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)