proposition: Lemma uniform_metric_complete: complete d -> complete uniform_metric.
proof: Proof. intros. rewrite @complete_net_limit_char with (X := MetricTopology d d_metric) in H. 2: apply MetricTopology_metrized. rewrite @complete_net_limit_char with (X := UniformTopology). 2: apply MetricTopology_metrized. assert (forall y:Net nat_DS (MetricTopology d d_metric), cauchy d y -> { y0:Y | net_limit y y0 }) as cauchy_limit. { intros. apply constructive_definite_description. apply -> unique_existence; split. - apply H; trivial. - apply (Hausdorff_impl_net_limit_unique y). apply T3_sep_impl_Hausdorff. apply normal_sep_impl_T3_sep. apply metrizable_impl_normal_sep. exists d; trivial; apply MetricTopology_metrized. } intros f ?. unshelve refine (let H1 := _ in let H2 := _ in ex_intro _ (exist _ (fun x:X => proj1_sig (cauchy_limit (fun n:nat => proj1_sig (f n) x) (H1 x))) H2) _); [ | clearbody H1 | clearbody H1 H2 ]. - intros. red; intros. destruct (H0 eps H1) as [N]. exists N; intros. apply Rle_lt_trans with (uniform_metric (f m) (f n)). + apply uniform_metric_bound_below. + apply H2; trivial. - assert (1 > 0) by (red; auto with real). destruct (H0 1 H2) as [N]. pose (fN := f N). assert (f N = fN) by reflexivity. destruct fN as [fN [M]]. assert (forall (n:nat) (x:X), (n >= N)%nat -> d (proj1_sig (f n) x) (proj1_sig (f N) x) < 1). { intros. apply uniform_metric_lt; auto. } assert (forall x:X, d (fN x) (proj1_sig (cauchy_limit _ (H1 x))) <= 1). { intros. apply lt_plus_epsilon_le. intros. destruct cauchy_limit; simpl. pose proof (metric_space_net_limit_converse _ _ (MetricTopology_metrized _ d d_metric) nat_DS (fun n:nat => proj1_sig (f n) x) x0 n). destruct (H7 eps H6) as [i0]. pose (N' := Nat.max N i0). apply Rle_lt_trans with (d (fN x) (proj1_sig (f N') x) + d x0 (proj1_sig (f N') x)). { rewrite metric_sym with (x:=x0) (y:=proj1_sig (f N') x); trivial. apply d_metric. } replace (fN x) with (proj1_sig (f N) x). 2: { rewrite H4; reflexivity. } assert (d (proj1_sig (f N) x) (proj1_sig (f N') x) < 1). { rewrite metric_sym; trivial. apply H5. lia. } assert (d x0 (proj1_sig (f N') x) < eps). { apply H8. simpl. lia. } auto with real. } exists (M+1). red; intros. destruct H7. rewrite H8; clear H8. apply Rle_trans with (d (y0 x) (fN x) + d (fN x) (proj1_sig (cauchy_limit _ (H1 x)))). { apply d_metric. } assert (d (y0 x) (fN x) <= M). { apply i. exists x; trivial. } auto with real. - apply metric_space_net_limit with uniform_metric. { apply MetricTopology_metrized. } intros. assert (eps/2 > 0) by lra. destruct (H0 (eps/2) H4) as [N]. exists N; intros. apply Rle_lt_trans with (eps/2); try lra. unfold uniform_metric; remember (f j) as fj; destruct fj as [fj]. destruct sup; simpl. apply i. red; intros. destruct H7. rewrite H8; clear y H8. apply lt_plus_epsilon_le; intros. destruct (cauchy_limit (fun n:nat => proj1_sig (f n) x0) (H1 x0)); simpl. pose proof (metric_space_net_limit_converse _ _ (MetricTopology_metrized _ d d_metric) nat_DS (fun n:nat => proj1_sig (f n) x0) x1 n). destruct (H9 eps0 H8) as [N']. pose (N'' := Nat.max N N'). apply Rle_lt_trans with (d x1 (proj1_sig (f N'') x0) + d (proj1_sig (f N'') x0) (proj1_sig (f j) x0)). { repeat rewrite <- Heqfj; simpl. apply d_metric. } assert (d x1 (proj1_sig (f N'') x0) < eps0). { apply H10. simpl. lia. } cut (d (proj1_sig (f N'') x0) (proj1_sig (f j) x0) < eps/2); [lra|]. apply Rle_lt_trans with (uniform_metric (f N'') (f j)). + unfold uniform_metric; destruct (f N'') as [f1]; destruct (f j) as [f2]; destruct sup; simpl. apply i0; exists x0; trivial. + apply H5; trivial. lia. Qed.
imports: MetricSpaces FunctionalExtensionality Completeness Description Max Psatz Lra