proposition: Lemma convergent_sequence_is_cauchy: forall (x:Net nat_DS X) (x0:point_set X), net_limit x x0 -> cauchy d x.
proof: Proof. intros. destruct (d_metrizes x0). red; intros. destruct (H (open_ball d x0 (eps/2))) as [N]. - Opaque In. apply open_neighborhood_basis_elements. Transparent In. constructor. lra. - constructor. rewrite metric_zero; trivial. lra. - simpl in N. exists N. intros. destruct (H1 m H2). destruct (H1 n H3). apply Rle_lt_trans with (d x0 (x m) + d x0 (x n)). + rewrite (metric_sym _ _ d_metric x0 (x m)); trivial. now apply triangle_inequality. + lra. Qed.
imports: Topology(SubspaceTopology) Psatz Coq(ProofIrrelevance)