proposition: Lemma metrizable_impl_T1_sep: forall X:TopologicalSpace, metrizable X -> T1_sep X.
proof: Proof. intros. destruct H. red. intros. rewrite <- closed_ball_radius_zero with (d := d); try assumption. apply metric_space_closed_ball_closed; assumption. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)