proposition: Lemma BanachCauchy: forall ϵ:Qpos, exists N, forall n m:nat , n >=N-> m>= N -> (ball ϵ (@Banach_seq _ F n x) (@Banach_seq _ F m x)).
proof: Proof. intros. set ceil:=(Qabs (approximate (d (@Banach_seq _ F 0 x) (@Banach_seq _ F 1 x)) (Qpos2QposInf (1#1))))+1:Qpos. exists ( /((ϵ*oneminc/ceil)(oneminc))). End BanachFPT. Section BanachFPT2. Context {X} (F:Complete X--> Complete X) `{conF: Contraction (Complete X) F}. Theorem BanachFPT : exists x, (F x) =x. eexists y. Admitted. Theorem PicardFPT: exists f, (Picard f) = (f ∘ Cunit). apply BanachFPT. Qed.
imports: CRtrans Qmetric ProductMetric CompleteProduct Unicode.Utf8 CPoly_Newton metric2.Classified Circle AbstractIntegration SimpleIntegration Qabs CRabs Interval CRGeometricSum