proposition: Lemma MetricTopology_metrized: forall (X:Type) (d:X->X->R) (d_metric: metric d), metrizes (MetricTopology d d_metric) d.
proof: Proof. intros. red. apply Build_TopologicalSpace_from_open_neighborhood_bases_basis. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)