proposition: Lemma cauchy_restriction (x : nat -> X) (HUx : forall n , In F (x n)) (Hx : cauchy d x) : cauchy d_restriction (fun n => exist F (x n) (HUx n)).
proof: Proof. intros eps Heps. destruct (Hx eps Heps) as [N HN]. exists N; intros. unfold d_restriction. simpl. auto. Qed.
imports: Topology(SubspaceTopology) Psatz Coq(ProofIrrelevance)