proposition: Lemma rationals_dense_in_RTop : @dense RTop (Im Full_set Q2R).
proof: Proof. eapply meets_every_nonempty_open_nbhd_basis_equiv_dense. { apply (fun x => RTop_metrization x). } intros x U [] _. destruct (rationals_dense_in_reals (x - r) (x + r)) as [q]. { lra. } exists (Q2R q). split. - apply Im_def. constructor. - do 2 red. constructor. unfold R_metric. apply Rabs_def1; lra. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals