proposition: Lemma dist_to_set_zero_impl_closure: forall x:X, dist_to_set d d_is_metric S S_nonempty x = 0 -> In (closure S) x.
proof: Proof. intros. apply NNPP; intro. destruct (d_metrizes_X x). destruct (open_neighborhood_basis_cond (Complement (closure S))) as [V [? ?]]. - split; trivial. apply closure_closed. - destruct H1 as [r]. unfold dist_to_set in H. destruct inf in H. simpl in H. rewrite H in i; clear x0 H. destruct i. assert (is_lower_bound (Im S (d x)) r). { red. intros y ?. destruct H4 as [y]. rewrite H5. clear y0 H5. destruct (total_order_T (d x y) r) as [[?|?]|?]; auto with real rorders. assert (In (open_ball d x r) y) by now constructor. apply H2 in H5. contradiction H5. now apply closure_inflationary. } apply H3 in H4. lra. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)