proposition: Lemma eitv_bnd_infty b r : `[r%:E, +oo[%classic = \bigcap_k [set` Interval (BSide b (r - k.+1%:R^-1)%:E) +oo%O] :> set _.
proof: Proof. rewrite predeqE => x; split=> [|]. - move: x => [s /=| _ n _|//]. + rewrite in_itv /= andbT lee_fin => rs n _ /=; rewrite in_itv/= andbT. case: b => /=. * by rewrite lee_fin lerBlDl (le_trans rs)// lerDr. * by rewrite lte_fin ltrBlDl (le_lt_trans rs)// ltrDr. + by rewrite /= in_itv /= andbT; case: b => /=; rewrite lteey. - move: x => [s| |/(_ 0%N Logic.I)] /=; rewrite ?in_itv/= ?leey//; last first. by case: b. move=> h; rewrite lee_fin leNgt andbT; apply/negP => /ltr_add_invr[k skr]. have {h} := h k Logic.I; rewrite /= in_itv /= andbT; case: b => /=. + by rewrite lee_fin lerBlDr leNgt skr. + by rewrite lte_fin ltrBlDr ltNge (ltW skr). 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