proposition: Lemma closed_subset_of_complete_is_complete: complete d -> closed F -> complete d_restriction.
proof: Proof. intros Hcomp HF. apply (complete_net_limit_char (SubspaceTopology F) d_restriction). { apply metric_space_subspace_topology_metrizes; auto. } rewrite complete_net_limit_char in Hcomp; auto. intros x Hx. pose (y := fun n:nat => proj1_sig (x n)). destruct (Hcomp y) as [y0 Hy0]. { red; intros eps Heps. destruct (Hx eps Heps) as [N]. now exists N. } - assert (In F y0) as HFy0. { rewrite <- (closure_fixes_closed _ HF); trivial. apply @net_limit_in_closure with (I:=nat_DS) (x:=y); trivial. apply exists_arbitrarily_large_all. intros ?. apply proj2_sig. } exists (exist _ y0 HFy0). apply metric_space_net_limit with d_restriction. + apply metric_space_subspace_topology_metrizes; auto. + intros. unfold d_restriction; simpl. apply metric_space_net_limit_converse; auto. Qed.
imports: Topology(SubspaceTopology) Psatz Coq(ProofIrrelevance)