proposition: Lemma metrizable_Hausdorff : forall X, metrizable X -> Hausdorff X.
proof: Proof. intros. red; intros. destruct H. exists (open_ball d x ((d x y)/2)). exists (open_ball d y ((d x y)/2)). assert (0 < d x y). { apply NNPP. intro. contradict H0. apply not_Rlt in H2. apply metric_strict with (d := d). { assumption. } apply Rle_antisym. + apply Rge_le. assumption. + apply Rge_le. apply metric_nonneg. assumption. } assert (d x y / 2 > 0). { apply Rdiv_lt_0_compat; try assumption. apply Rlt_0_2. } repeat split. - apply metric_space_open_ball_open; assumption. - apply metric_space_open_ball_open; assumption. - rewrite metric_zero; assumption. - rewrite metric_zero; assumption. - apply Extensionality_Ensembles; split; red; intros. 2: { contradiction. } destruct H4. destruct H4, H5. assert (d x x0 + d x0 y < d x y). { rewrite double_var. apply Rplus_lt_compat; try assumption. rewrite metric_sym; assumption. } pose proof (triangle_inequality _ _ H x x0 y). pose proof (Rle_lt_trans _ _ _ H7 H6). apply Rlt_irrefl in H8. contradiction. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)