proposition: Lemma eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R).
proof: Proof. rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry. move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=. rewrite andbT lte_fin ltNge. have [r0|r0] := ltP 0%R r; last by rewrite (le_trans r0). by rewrite natr_absz gtr0_norm // ?ceil_ge// ceil_gt0. 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