proposition: Lemma punct_eitv_bndy b y : [set` Interval (BSide b y%:E) +oo%O] = EFin @` [set` Interval (BSide b y) +oo%O] `|` [set +oo].
proof: Proof. rewrite predeqE => x; split; rewrite /= in_itv andbT. - move: x => [x| |] yxb; [|by right|by case: b yxb]. by left; exists x => //; rewrite in_itv /= andbT; case: b yxb. - move=> [[r]|->]. + by rewrite in_itv /= andbT => yxb <-; case: b yxb. + by case: b => /=; rewrite ?(ltry, leey). 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