proposition: Lemma sfinite_measure_sigma_finite d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) : sigma_finite setT mu -> sfinite_measure mu.
proof: Proof. move=> [F UF mF]; rewrite /sfinite_measure. have mDF k : measurable (seqDU F k). apply: measurableD; first exact: (mF k).1. by apply: bigsetU_measurable => i _; exact: (mF i).1. exists (fun k => [the measure _ _ of mrestr mu (mDF k)]) => [n|U mU]. - apply: lty_fin_num_fun => //=. rewrite /mrestr setTI (@le_lt_trans _ _ (mu (F n)))//. + apply: le_measure; last exact: subDsetl. * rewrite inE; apply: measurableD; first exact: (mF n).1. by apply: bigsetU_measurable => i _; exact: (mF i).1. * by rewrite inE; exact: (mF n).1. + exact: (mF n).2. rewrite /mseries/= /mrestr/=; apply/esym/cvg_lim => //. rewrite -[X in _ --> mu X]setIT UF seqDU_bigcup_eq setI_bigcupr. apply: (@measure_sigma_additive _ _ _ mu (fun k => U `&` seqDU F k)). by move=> i; exact: measurableI. exact/trivIset_setIl/trivIset_seqDU. 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)