proposition: Lemma RmuE (A : set T) : measurable A -> Rmu A = mu A.
proof: Proof. move=> Am; rewrite -[A in LHS](@bigcup_set1 _ unit _ tt). by rewrite Rmu_fin_bigcup// ?fsbig_set1// => -[]. 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)