proposition: Lemma complete_net_limit_char : complete d <-> forall x:nat -> X, cauchy d x -> exists x0:X, net_limit x x0 (I:=nat_DS).
proof: Proof. split; intros Hcomp; intros x Hx; specialize (Hcomp x Hx) as [x0 Hx0]; exists x0. - eapply metric_space_net_limit; eauto. - intros eps Heps. eapply metric_space_net_limit_converse in Hx0; eauto. Qed.
imports: Topology(SubspaceTopology) Psatz Coq(ProofIrrelevance)