proposition: Lemma semiring_sigma_additive : sigma_sub_additive mu -> semi_sigma_additive mu.
proof: Proof. move=> /ring_semi_sigma_additive Rmu_sigmadd F Fmeas Ftriv cupFmeas. have Fringmeas i : d.-ring.-measurable (F i) by apply: measurable_subring. have := Rmu_sigmadd F Fringmeas Ftriv (measurable_subring cupFmeas). rewrite SetRing.RmuE//. by under eq_fun do under eq_bigr do rewrite SetRing.RmuE//=. 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)