proposition: Lemma sigma_finiteP : sigma_finite A mu <-> exists F, [/\ A = \bigcup_i F i, nondecreasing_seq F & forall i, measurable (F i) /\ mu (F i) < +oo].
proof: Proof. split=> [[F AUF mF]|[F [? ? ?]]]; last by exists F. exists (fun n => \big[setU/set0]_(i < n.+1) F i); split. - rewrite AUF; apply/seteqP; split. by apply: subset_bigcup => i _; exact: bigsetU_sup. by apply: bigcup_sub => i _; exact: bigsetU_bigcup. - by move=> i j ij; exact/subsetPset/subset_bigsetU. - move=> i; split; first by apply: bigsetU_measurable => j _; exact: (mF j).1. rewrite (le_lt_trans (Boole_inequality _ _))//. by move=> j _; exact: (mF _).1. by apply/lte_sum_pinfty => j _; exact: (mF j).2. 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)