proposition: Lemma EFin_itv_bnd_infty b r : EFin @` [set` Interval (BSide b r) +oo%O] = [set` Interval (BSide b r%:E) +oo%O] `\ +oo.
proof: Proof. rewrite eqEsubset; split => [x [s /itvP rs <-]|x []]. split => //=; rewrite in_itv /=. by case: b in rs *; rewrite /= ?(lee_fin, lte_fin) rs. move: x => [s|_ /(_ erefl)|] //=; rewrite in_itv /= andbT; last first. by case: b => /=; rewrite 1?(leNgt,ltNge) 1?(ltNyr, leNye). by case: b => /=; rewrite 1?(lte_fin,lee_fin) => rs _; exists s => //; rewrite in_itv /= rs. 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