proposition: Lemma metrizable_impl_normal_sep: forall X:TopologicalSpace, metrizable X -> normal_sep X.
proof: Proof. intros. split. { apply metrizable_impl_T1_sep. assumption. } destruct H. intros. case (classic_dec (Inhabited F)); intro. 2: { apply Powerset_facts.not_inhabited_empty in n. subst. exists Empty_set, Full_set. repeat split; auto with sets topology. } case (classic_dec (Inhabited G)); intro. 2: { apply Powerset_facts.not_inhabited_empty in n. subst. exists Full_set, Empty_set. repeat split; auto with sets topology. } pose (U := [ x:X | dist_to_set d H F i x < dist_to_set d H G i0 x ]). pose (V := [ x:X | dist_to_set d H G i0 x < dist_to_set d H F i x ]). exists U, V; repeat split. - now apply closer_to_S_than_T_open. - now apply closer_to_S_than_T_open. - replace (dist_to_set d H F i x) with 0. + destruct (total_order_T 0 (dist_to_set d H G i0 x)) as [[?|?]|?]; trivial. * symmetry in e. apply dist_to_set_zero_impl_closure in e; trivial. rewrite closure_fixes_closed in e; trivial. assert (In Empty_set x). { rewrite <- H3. now constructor. } destruct H5. * destruct (Rlt_irrefl 0). apply Rle_lt_trans with (dist_to_set d H G i0 x); auto with sets. unfold dist_to_set. destruct inf. simpl. apply i1. red. intros. destruct H5. rewrite H6. now apply metric_nonneg. + unfold dist_to_set. destruct inf. simpl. apply Rle_antisym. * apply i1. red. intros. destruct H5. rewrite H6. now apply metric_nonneg. * destruct i1. assert (0 >= x0); auto with real. apply H5. exists x; trivial. rewrite metric_zero; auto with real. - replace (dist_to_set d H G i0 x) with 0. + destruct (total_order_T 0 (dist_to_set d H F i x)) as [[?|?]|?]; trivial. * symmetry in e. apply dist_to_set_zero_impl_closure in e; trivial. rewrite closure_fixes_closed in e; trivial. now assert (In Empty_set x) by now rewrite <- H3. * destruct (Rlt_irrefl 0). apply Rle_lt_trans with (dist_to_set d H F i x); auto with real. unfold dist_to_set. destruct inf. simpl. apply i1. red. intros. destruct H5. rewrite H6. now apply metric_nonneg. + symmetry. apply closure_impl_dist_to_set_zero; trivial. now apply closure_inflationary. - extensionality_ensembles; lra. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)