proposition: Lemma emeasurable_itv (i : interval (\bar R)) : measurable ([set` i]%classic : set \bar R).
proof: Proof. rewrite -[X in measurable X]setCK; apply: measurableC. rewrite set_interval.setCitv /=; apply: measurableU => [|]. - by move: i => [[b1 i1|[|]] i2] /=; rewrite ?set_interval.set_itvE. - by move: i => [i1 [b2 i2|[|]]] /=; rewrite ?set_interval.set_itvE. 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