proposition: Lemma semi_sigma_additive_is_additive d (T : semiRingOfSetsType d) (R : realFieldType) (mu : set T -> \bar R) : mu set0 = 0 -> semi_sigma_additive mu -> semi_additive mu.
proof: Proof. move=> mu0 samu A n Am Atriv UAm. have := samu (fun i => if (i < n)%N then A i else set0). rewrite (bigcup_splitn n) bigcup0 ?setU0; last first. by move=> i _; rewrite -ltn_subRL subnn. under eq_bigr do rewrite ltn_ord. move=> /(_ _ _ UAm)/(@cvg_lim _) <-//; last 2 first. - by move=> i; case: ifP. - move=> i j _ _; do 2![case: ifP] => ? ?; do ?by rewrite (setI0, set0I) => -[]. by move=> /Atriv; apply. apply: lim_near_cst => //=; near=> i. have /subnKC<- : (n <= i)%N by near: i; exists n. transitivity (\sum_(j < n + (i - n)) mu (if (j < n)%N then A j else set0)). by rewrite big_mkord. rewrite big_split_ord/=; under eq_bigr do rewrite ltn_ord. by rewrite [X in _ + X]big1 ?adde0// => ?; rewrite -ltn_subRL subnn. Unshelve. all: by end_near. 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)