proposition: Lemma completion_exists_nondense : exists (Y : Type) (d' : Y -> Y -> R) (d'_metric : metric d') (i : X -> Y), isometry d d' i /\ complete d'.
proof: Proof. destruct (classic (inhabited X)). 2: { unshelve eexists False, (False_rect _), _, _. 3: split. - constructor; intros; contradiction. - intros x; apply H; constructor; apply x. - intros ? ?; contradict H; constructor; auto. - intros x; contradiction (x 0%nat). } destruct H as [x0]. exists (uniform_space R_metric (d x0)), (uniform_metric R_metric (d x0) R_metric_is_metric (inhabits x0)), (uniform_metric_is_metric _ _ _ _ _ _). unshelve refine (let H0:=_ in ex_intro _ (fun x:X => exist _ (d x) (H0 x)) _); [|split]. * intros. exists (d x0 x). intros x1 Hx1. destruct Hx1. subst. apply metric_alternate_triangle_ineq. * red; intros x1 x2. unfold uniform_metric. destruct sup as [? i]; simpl. apply Rle_antisym; apply i. -- red; intros x3 Hx3. destruct Hx3. subst. apply metric_alternate_triangle_ineq. -- exists x1; [constructor|]. rewrite metric_zero; auto. rewrite (metric_sym _ _ d_metric x2 x1). unfold R_metric. rewrite Rminus_0_r. symmetry; apply Rabs_right, metric_nonneg, d_metric. * apply uniform_metric_complete. apply R_metric_complete. Qed.
imports: Coq(Description ProofIrrelevance Psatz) Topology(UniformTopology RTopology)