proposition: Lemma open_ereal_lt_ereal x : open [set y | y < x].
proof: Proof. have openr r : open [set x : \bar R | x < r%:E]. move=> [? | // | ?]; [rewrite /= lte_fin => xy | by exists r]. by move: (@open_ereal_lt r%:E); rewrite openE; apply; rewrite /= lte_fin. move: x => [ // | | ]; last by move=> []. suff -> : [set y | y < +oo] = \bigcup_r [set y : \bar R | y < r%:E]. exact: bigcup_open. rewrite predeqE => -[r | | ]/=. - rewrite ltry; split => // _. by exists (r + 1)%R => //=; rewrite lte_fin ltrDl. - by rewrite ltxx; split => // -[] x /=; rewrite ltNge leey. - by split => // _; exists 0%R => //=; rewrite ltNye. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule