proposition: Lemma R_metric_complete: complete R_metric.
proof: Proof. apply complete_cauchy_cluster_points with (X := RTop). 1: apply R_metric_is_metric. 1: apply RTop_metrization. intros x Hx. pose proof (cauchy_impl_bounded _ R_metric_is_metric x Hx) as [p [r Hpr]]. destruct (bounded_real_net_has_cluster_point nat_DS x (p - r) (p + r)) as [x0]. { intros n. unshelve epose proof (Hpr (x n) _) as [Hn]. { apply Im_def. constructor. } unfold R_metric, Rabs in Hn. destruct (Rcase_abs _); lra. } exists x0. assumption. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals