proposition: Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable.
proof: Proof. apply/seteqP; split; last first. apply: smallest_sub. split; first exact: emeasurable0. by move=> *; rewrite setTD; exact: emeasurableC. by move=> *; exact: bigcupT_emeasurable. move=> _ [r ->]/=; exists `[r, +oo[%classic. rewrite RGenOInfty.measurableE. exact: RGenOInfty.measurable_itv_bnd_infty. by exists [set +oo]; [constructor|rewrite -punct_eitv_bndy]. move=> _ [A' mA' [C mC]] <-; apply: measurableU; last first. case: mC; [by []|exact: measurable_set1Ny| exact: measurable_set1y|]. by apply: measurableU; [exact: measurable_set1Ny|exact: measurable_set1y]. rewrite RGenCInfty.measurableE in mA'. have smA' := smallest_sub _ _ mA'. apply: (smA' (G.-sigma.-measurable \o (image^~ EFin))); last first. move=> _ [r ->]/=; rewrite EFin_itv_bnd_infty; apply: measurableD. by apply: sub_sigma_algebra => /=; exists r. exact: measurable_set1y. split=> /= [|D mD|F mF]; first by rewrite image_set0. - rewrite setTD EFin_setC; apply: measurableD; first exact: measurableC. by apply: measurableU; [exact: measurable_set1Ny|exact: measurable_set1y]. - by rewrite EFin_bigcup; apply: bigcup_measurable => i _; exact: mF. 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