proposition: Lemma R_bounded_char (U : Ensemble R) : bounded R_metric U <-> Coq.Reals.Rtopology.bounded U.
proof: Proof. unfold bounded, Rtopology.bounded. split. - intros [x [r H]]. exists (x-r-1), (x+r+1). intros y Hy. specialize (H y Hy). destruct H. unfold R_metric in H. unfold Rabs in H. destruct (Rcase_abs _); lra. - intros [m [M H]]. exists ((m+M)/2), (M-m+1). intros y Hy. specialize (H y Hy). constructor. unfold R_metric, Rabs. destruct (Rcase_abs _); lra. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals