fact: Definition cauchy (x:nat->X) : Prop := forall eps:R, eps > 0 -> exists N:nat, forall m n:nat, (m >= N)%nat -> (n >= N)%nat -> d (x m) (x n) < eps.
imports: Topology(SubspaceTopology) Psatz Coq(ProofIrrelevance)