proposition: Lemma RTop_subbasis_rational_beams : subbasis (Union (ImageFamily (fun q => [r : RTop | r < Q2R q])) (ImageFamily (fun q => [r : RTop | r > Q2R q]))).
proof: Proof. split. - intros S H. destruct H as [S [[q Hq] H]| S [[q Hq] H]]; subst. + apply R_lower_beam_open. + apply R_upper_beam_open. - intros U r H1 H2. assert (neighborhood U r) as H by now exists U. apply RTop_neighborhood_is_neighbourhood in H. destruct H as [[d ?] H], (rationals_dense_in_reals (r - d) r) as [p ?], (rationals_dense_in_reals r (r + d)) as [q ?]; exists (Intersection [x : R | x > Q2R p] [x : R | x < Q2R q]) + lra. repeat split; simpl; try lra. + do 2 constructor; [ right | left ]; repeat econstructor. + intros ? [y [?] [?]]. apply H, Rabs_def1; simpl; lra. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals