proposition: Corollary metrizable_SubspaceTopology {X : TopologicalSpace} (F : Ensemble X) : metrizable X -> metrizable (SubspaceTopology F).
proof: Proof. intros [d Hd HXd]. eexists. - eapply d_restriction_metric. eassumption. - apply metric_space_subspace_topology_metrizes; auto. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)