proposition: Lemma eitv_infty_bnd b r : `]-oo, r%:E]%classic = \bigcap_k [set` Interval -oo%O (BSide b (r%:E + k.+1%:R^-1%:E))] :> set _.
proof: Proof. rewrite predeqE => x; split=> [|]. - move: x => [s /=|//|_ n _]. + rewrite in_itv /= lee_fin => sr n _; rewrite /= in_itv /= -EFinD. case: b => /=. * by rewrite lte_fin (le_lt_trans sr)// ltrDl. * by rewrite lee_fin (le_trans sr)// lerDl. + by rewrite /= in_itv /= -EFinD; case: b => //=; rewrite lteNye. - move: x => [s|/(_ 0%N Logic.I)|]/=; rewrite !in_itv/= ?leNye//; last first. by case: b. move=> h; rewrite lee_fin leNgt; apply/negP => /ltr_add_invr[k rks]. have {h} := h k Logic.I; rewrite /= in_itv /= -EFinD; case: b => /=. + by rewrite lte_fin ltNge (ltW rks). + by rewrite lee_fin leNgt rks. 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