proposition: Lemma extension_approximation_seq_cauchy_aux: forall (m n:nat) (x:X), Rabs (proj1_sig (extension_approximation_seq m) x - proj1_sig (extension_approximation_seq n) x) <= Rabs ((2/3)^m - (2/3)^n).
proof: Proof. cut (forall (m n:nat) (x:X), (m <= n)%nat -> Rabs (proj1_sig (extension_approximation_seq m) x - proj1_sig (extension_approximation_seq n) x) <= (2/3)^m - (2/3)^n). - intros. destruct (Nat.le_gt_cases m n). + rewrite (Rabs_right ((2/3)^m - (2/3)^n)). { now apply H. } apply Rge_minus. cut ((2/3)^n <= (2/3)^m); auto with real. apply Rle_R1_pow; trivial. lra. + apply Nat.lt_le_incl in H0. rewrite (Rabs_left1 ((2/3)^m - (2/3)^n)). * replace (- ((2/3)^m - (2/3)^n)) with ((2/3)^n - (2/3)^m) by ring. rewrite Rabs_minus_sym. now apply H. * apply Rle_minus. apply Rle_R1_pow; trivial. lra. - induction 1. + repeat match goal with |- context [ ?y - ?y ] => replace (y-y) with 0 by ring end. rewrite Rabs_R0. lra. + simpl pow. apply Rle_trans with (Rabs (proj1_sig (extension_approximation_seq m) x - proj1_sig (extension_approximation_seq m0) x) + Rabs (proj1_sig (extension_approximation_seq m0) x - proj1_sig (extension_approximation_seq (S m0)) x)). * rewrite Rplus_comm. apply R_metric_is_metric. * pose proof (extension_approximation_seq_diff m0 x). cut (Rabs (proj1_sig (extension_approximation_seq m0) x - proj1_sig (extension_approximation_seq (S m0)) x) <= 1/3 * (2/3)^m0). { lra. } destruct H0. unfold Rabs. destruct Rcase_abs; lra. Qed.
imports: RTopology SeparatednessAxioms RFuncContinuity UniformTopology ContinuousFactorization Coq(Description Max Psatz ClassicalChoice) ZornsLemma(Proj1SigInjective) UrysohnsLemma