proposition: Lemma measurable_Rmu_extE d (R : realType) (T : semiRingOfSetsType d) (mu : {measure set T -> \bar R}) X : d.-ring.-measurable X -> mu^* X = SetRing.measure mu X.
proof: Proof. by move=> Xm/=; rewrite -Rmu_ext/= measurable_mu_extE. 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)