proposition: Lemma measurable_er_map d (T : measurableType d) (R : realType) (f : R -> R) : measurable_fun setT f -> measurable_fun [set: \bar R] (er_map f).
proof: Proof. move=> mf;rewrite (_ : er_map _ = fun x => if x \is a fin_num then (f (fine x))%:E else x); last first. by apply: funext=> -[]. apply: measurable_fun_ifT => //=. + apply: (measurable_fun_bool true). rewrite /preimage/= -[X in measurable X]setTI. exact/emeasurable_fin_num. + exact/EFin_measurable_fun/measurableT_comp. 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