proposition: Lemma extension_approximation_seq_diff: forall (n:nat) (x:X), -(1/3 * (2/3)^n) <= proj1_sig (extension_approximation_seq (S n)) x - proj1_sig (extension_approximation_seq n) x <= 1/3*(2/3)^n.
proof: Proof. intros. simpl extension_approximation_seq. destruct extension_approximation_seq. simpl. match goal with |- context [extension_approximation ?A ?B x] => cut (-1/3 <= extension_approximation A B x <= 1/3); [ generalize (extension_approximation A B x) | apply extension_approximation_bound ] end. intros. assert (0 <= (2/3)^n). { apply pow_le. lra. } replace (-(1/3*(2/3)^n)) with ((2/3)^n*(-1/3)) by field. replace (1/3*(2/3)^n) with ((2/3)^n*(1/3)) by ring. replace (x0 x + (2/3)^n*p - x0 x) with ((2/3)^n*p) by ring. destruct H. split; now apply Rmult_le_compat_l. Qed.
imports: RTopology SeparatednessAxioms RFuncContinuity UniformTopology ContinuousFactorization Coq(Description Max Psatz ClassicalChoice) ZornsLemma(Proj1SigInjective) UrysohnsLemma