proposition: Theorem completion_exists: exists (Y:TopologicalSpace) (i : X -> Y) (d' : Y -> Y -> R) (d'_metric : metric d'), metrizes Y d' /\ dense (Im Full_set i) /\ isometry d d' i /\ complete d'.
proof: Proof. intros. destruct completion_exists_nondense as [Y [d' [d'_metric [i [Hi_iso d'_comp]]]]]. pose (F := closure (Im Full_set i) (X:=MetricTopology d' d'_metric)). exists (SubspaceTopology F). assert (forall x:X, In F (i x)) as HFi. { intros. apply closure_inflationary. exists x; trivial. constructor. } exists (fun x:X => exist _ (i x) (HFi x)). pose (d'' := fun y1 y2 : SubspaceTopology F=> d' (proj1_sig y1) (proj1_sig y2)). exists d''. assert (d'_metric0 : metric d''). { apply d_restriction_metric. assumption. } assert (d'_metrizes0 : metrizes _ d''). { apply metric_space_subspace_topology_metrizes; auto. apply MetricTopology_metrized. } exists d'_metric0. split; auto. repeat split. 2: { intros ? ?. simpl. apply Hi_iso. } 2: { apply (@closed_subset_of_complete_is_complete (MetricTopology d' d'_metric) d' d'_metric (MetricTopology_metrized _ d' d'_metric) F d'_comp (closure_closed _) ). } pose proof (@dense_in_closure (MetricTopology d' d'_metric) (Im Full_set i)). match goal with | H : dense ?a |- dense ?b => replace b with a; auto end. apply Extensionality_Ensembles; split; red. - intros [x Hx0] [Hx1]. simpl in Hx1. inversion Hx1; subst; clear Hx1. exists x0; auto. apply subset_eq_compat; auto. - intros [x Hx0] ?. inversion H0; subst; clear H0. constructor. simpl. exists x0; [constructor|]. inversion H2; subst; clear H2; auto. Qed.
imports: Coq(Description ProofIrrelevance Psatz) Topology(UniformTopology RTopology)