proposition: Lemma complete_subset_is_closed: complete d_restriction -> closed F.
proof: Proof. intros. cut (Included (closure F) F). { intros. assert (closure F = F) as H1. { apply Extensionality_Ensembles. split; trivial; apply closure_inflationary. } rewrite <- H1; apply closure_closed. } red; intros. assert (exists y:Net nat_DS X, (forall n:nat, In F (y n)) /\ net_limit y x) as [y [HyF Hyx]]. { apply first_countable_sequence_closure; trivial. apply metrizable_impl_first_countable. exists d; trivial. } pose (y' := ((fun n:nat => exist _ (y n) (HyF n)) : Net nat_DS (SubspaceTopology F))). assert (cauchy d_restriction y') as Hy'. { apply cauchy_restriction; auto. apply convergent_sequence_is_cauchy with x; trivial. } destruct (H y' Hy') as [[x0 Hx0] Hy'x0]. cut (net_limit y x0). - intros Hyx0. assert (x = x0). { eapply Hausdorff_impl_net_limit_unique; eauto. apply metrizable_Hausdorff. exists d; auto. } congruence. - apply metric_space_net_limit with d; auto. Qed.
imports: Topology(SubspaceTopology) Psatz Coq(ProofIrrelevance)