proposition: Lemma extension_approximation_seq_cauchy: cauchy (uniform_metric R_metric (fun _:X => 0) R_metric_is_metric X_nonempty) convert_approx_to_uniform_space.
proof: Proof. red. intros. assert (Rabs (2/3) < 1). { rewrite Rabs_right; lra. } assert (0 < eps/2) by lra. destruct (pow_lt_1_zero (2/3) H0 (eps/2) H1) as [N]. exists N. intros. apply Rle_lt_trans with (Rabs ((2/3)^m - (2/3)^n)). - unfold uniform_metric, convert_approx_to_uniform_space. destruct sup. simpl. apply i. red. intros. destruct H5. rewrite H6. clear y H6. rewrite metric_sym. + apply extension_approximation_seq_cauchy_aux. + exact R_metric_is_metric. - apply Rle_lt_trans with (Rabs ((2/3)^m) + Rabs((2/3)^n)). + rewrite <- (Rabs_Ropp ((2/3)^n)). unfold Rminus. apply Rabs_triang. + replace eps with (eps/2 + eps/2) by field. apply Rplus_lt_compat; now apply H2. Qed.
imports: RTopology SeparatednessAxioms RFuncContinuity UniformTopology ContinuousFactorization Coq(Description Max Psatz ClassicalChoice) ZornsLemma(Proj1SigInjective) UrysohnsLemma