proposition: Lemma emeasurableC (X : set \bar R) : emeasurable X -> emeasurable (~` X).
proof: Proof. move => -[A mA] [B PooB <-]; rewrite setCU setCU_Efin //. exists (~` A); [exact: measurableC | exists ([set -oo%E; +oo%E] `&` ~` B) => //]. case: PooB. - by rewrite setC0 setIT; constructor. - rewrite setIUl setICr set0U -setDE. have [_ ->] := @setDidPl (\bar R) [set +oo%E] [set -oo%E]; first by constructor. by rewrite predeqE => x; split => // -[->]. - rewrite setIUl setICr setU0 -setDE. have [_ ->] := @setDidPl (\bar R) [set -oo%E] [set +oo%E]; first by constructor. by rewrite predeqE => x; split => // -[->]. - by rewrite setICr; constructor. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure