proposition: Lemma RTop_metrization: metrizes RTop R_metric.
proof: Proof. pose proof (Hsubbasis := Build_TopologicalSpace_from_subbasis_subbasis _ (order_topology_subbasis _ Rle)). red. intros. constructor; intros. - destruct H. replace (@open_ball RTop R_metric x r) with (Intersection [ y:R | x-r <= y /\ y <> x-r ] [ y:R | y <= x+r /\ y <> x+r ]). + constructor. * apply (@open_intersection2 RTop); apply Hsubbasis; constructor. * repeat constructor; lra. + extensionality_ensembles; repeat constructor; try apply Rabs_def2 in H0; destruct H0; try lra. destruct H1. apply Rabs_def1; lra. - intros. apply open_neighborhood_is_neighborhood, RTop_neighborhood_is_neighbourhood in H. destruct H. exists (open_ball R_metric x x0). split. + now destruct x0. + intros r [H0]. now apply H. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals