proposition: Lemma Rmu_ext d (R : realType) (T : semiRingOfSetsType d) (mu : {content set T -> \bar R}) : (measure mu)^* = mu^*.
proof: Proof. apply/funeqP => /= X; rewrite /mu_ext/=; apply/eqP; rewrite eq_le. rewrite ?lb_ereal_inf// => _ [F [Fm XS] <-]; rewrite ereal_inf_lb//; last first. exists F; first by split=> // i; apply: sub_gen_smallest. by rewrite (eq_eseriesr (fun _ _ => RmuE _ (Fm _))). pose K := [set: nat] `*`` fun i => decomp (F i). have /ppcard_eqP[f] : (K #= [set: nat])%card. apply: cardMR_eq_nat => // i; split; last by apply/set0P; rewrite decompN0. by apply: finite_set_countable => //; exact: decomp_finite_set. pose g i := (f^-1%FUN i).2; exists g; first split. - move=> k; have [/= _ /mem_set] : K (f^-1%FUN k) by apply: funS. exact: decomp_measurable. - move=> i /XS [k _]; rewrite -[F k]cover_decomp => -[D /= DFk Di]. by exists (f (k, D)) => //; rewrite /g invK// inE. rewrite !nneseries_esum//= /measure ?set_true. transitivity (\esum_(i in setT) \sum_(X0 \in decomp (F i)) mu X0); last first. by apply: eq_esum => /= k _; rewrite fsbig_finite//; exact: decomp_finite_set. rewrite -(eq_esum (fun _ _ => esum_fset _ _))//; last first. by move=> ? _; exact: decomp_finite_set. rewrite esum_esum//= (reindex_esum K setT f) => //=. by apply: eq_esum => i Ki; rewrite /g funK ?inE. 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)