proposition: Corollary MetricTopology_metrizable X (d:X->X->R) d_metric : metrizable (MetricTopology d d_metric).
proof: Proof. apply intro_metrizable with (d := d). - assumption. - apply MetricTopology_metrized. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)