proposition: Lemma measure_extension_sigma_finite : @sigma_finite _ T _ setT mu -> @sigma_finite _ _ _ setT measure_extension.
proof: Proof. move=> -[S setTS mS]; exists S => //; move=> i; split. by have := (mS i).1; exact: sub_sigma_algebra. by rewrite /measure_extension /= measurable_mu_extE //; [exact: (mS i).2 | exact: (mS i).1]. 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)