proposition: Lemma dist_to_set_triangle_inequality: forall (x y:X), dist_to_set y <= dist_to_set x + d x y.
proof: Proof. intros. unfold dist_to_set at 1. destruct inf as [dSy [? ?]]. simpl. unfold dist_to_set at 1. destruct inf as [dSx]. simpl. clear r. apply lt_plus_epsilon_le. intros. destruct (glb_approx _ _ _ i0 H) as [dxz [[z]]]. rewrite H1 in H2. clear y0 H1. destruct H2. apply Rle_lt_trans with (d y z). - assert (d y z >= dSy); auto with real. apply i. now exists z. - eapply Rle_lt_trans. + now apply triangle_inequality. + rewrite (metric_sym _ _ d_is_metric y x). lra. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)