proposition: Lemma closer_to_S_than_T_open: open [x:X | dist_to_set d d_is_metric S S_nonempty x < dist_to_set d d_is_metric T T_nonempty x].
proof: Proof. apply open_char_neighborhood. intros. destruct H. match type of H with ?d1 < ?d2 => pose (eps := d2 - d1) end. exists (open_ball d x (eps/2)). split. { split. - apply metric_space_open_ball_open; assumption. - apply metric_open_ball_In; try assumption. assert (0 < eps). { apply Rgt_minus. auto with real. } lra. } intros ? ?. destruct H0. constructor. eapply Rle_lt_trans with (dist_to_set d d_is_metric S S_nonempty x + d x x0). - apply dist_to_set_triangle_inequality. - apply Rlt_le_trans with (dist_to_set d d_is_metric T T_nonempty x - d x x0). * apply Rminus_lt. match goal with |- ?LHS < 0 => replace LHS with (2 * d x x0 - eps) end; [| unfold eps]; lra. * assert (dist_to_set d d_is_metric T T_nonempty x <= dist_to_set d d_is_metric T T_nonempty x0 + d x x0). { rewrite (metric_sym _ d d_is_metric x x0). apply dist_to_set_triangle_inequality. } lra. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)