proposition: Lemma measurable_image_fine (X : set \bar R) : measurable X -> measurable [set fine x | x in X `\` [set -oo; +oo]%E].
proof: Proof. case => Y mY [X' [ | <-{X} | <-{X} | <-{X} ]]. - rewrite setU0 => <-{X}. rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. by move=> [x [[x' Yx' <-{x}/= _ <-//]]]. by move=> Yr; exists r%:E; split => [|[]//]; exists r. - rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. move=> [x [[[x' Yx' <- _ <-//]|]]]. by move=> <-; rewrite not_orP => -[]/(_ erefl). by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. - rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. move=> [x [[[x' Yx' <-{x} _ <-//]|]]]. by move=> ->; rewrite not_orP => -[_]/(_ erefl). by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. - rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. by rewrite setDUl setDv setU0 => -[_ [[x' Yx' <-]] _ <-]. by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. 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