proposition: Lemma open_ereal_gt_ereal x : open [set y | x < y].
proof: Proof. have openr r : open [set x | r%:E < x]. move=> [? | ? | //]; [rewrite /= lte_fin => xy | by exists r]. by move: (@open_ereal_gt r%:E); rewrite openE; apply; rewrite /= lte_fin. case: x => [ // | | ]; first by move=> []. suff -> : [set y | -oo < y] = \bigcup_r [set y : \bar R | r%:E < y]. exact: bigcup_open. rewrite predeqE => -[r | | ]/=. - rewrite ltNyr; split => // _. by exists (r - 1)%R => //=; rewrite lte_fin ltrBlDr ltrDl. - by split => // _; exists 0%R => //=; rewrite ltey. - by rewrite ltxx; split => // -[] x _ /=; rewrite ltNge leNye. 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