proposition: Lemma cauchy_sequence_with_cluster_point_converges: forall (x:Net nat_DS X) (x0:point_set X), cauchy d x -> net_cluster_point x x0 -> net_limit x x0.
proof: Proof. intros x x0 Hx Hx0. apply metric_space_net_limit with d; auto. intros. red; intros. destruct (Hx (eps/2)) as [N HN]. { lra. } pose (U := open_ball d x0 (eps/2)). assert (open_neighborhood U x0) as [HU0 HU1]. { unfold U. split; auto. - apply metric_space_open_ball_open; auto. - apply metric_open_ball_In; auto; lra. } destruct (Hx0 U HU0 HU1 N) as [m [Hm [Hxm]]]. simpl in m, Hm. exists N; intros n Hn. simpl in n, Hn. apply Rle_lt_trans with (d x0 (x m) + d (x m) (x n)). - now apply triangle_inequality. - cut (d (x m) (x n) < eps/2). + lra. + now apply HN. Qed.
imports: Topology(SubspaceTopology) Psatz Coq(ProofIrrelevance)