proposition: Lemma closure_impl_dist_to_set_zero: forall x:X, In (closure S) x -> dist_to_set d d_is_metric S S_nonempty x = 0.
proof: Proof. intros. unfold dist_to_set; destruct inf. destruct i. simpl. apply Rle_antisym. - apply lt_plus_epsilon_le. intros. ring_simplify. assert (exists y:X, In S y /\ d x y < eps). { apply NNPP; intro. pose proof (not_ex_all_not _ _ H1). clear H1. simpl in H2. assert (In (interior (Complement S)) x). { exists (open_ball d x eps). - red. split. destruct (d_metrizes_X x). destruct (open_neighborhood_basis_elements (open_ball d x eps)). + constructor. lra. + split; trivial. red. intros y ?. destruct H4. red; red; intro. contradiction (H2 y). now split. - constructor. now rewrite metric_zero. } rewrite interior_complement in H1. now contradiction H1. } destruct H1 as [y [? ?]]. assert (d x y >= x0). { apply i. now exists y. } lra. - apply r. red. intros. destruct H0. rewrite H1. now apply metric_nonneg. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)