proposition: Lemma applyPointwiseLimit : forall {R : ConstructiveReals} {X : Set} (fn : nat -> PartialFunction X) (x : X) (xD : Domain (XpointwiseLimit fn) x) (a : CRcarrier R), prod (partialApply (XpointwiseLimit fn) x xD == a -> CR_cv _ (fun n => partialApply (fn n) x (let (xn, _) := xD in xn n)) a) (CR_cv _ (fun n => partialApply (fn n) x (let (xn, _) := xD in xn n)) a -> partialApply (XpointwiseLimit fn) x xD == a).
proof: Proof. intros. simpl. destruct xD. destruct (CR_complete R (fun n : nat => partialApply (fn n) x (x0 n)) c). split. - intros. exact (CR_cv_proper _ x1 a c0 H). - intros. apply (CR_cv_unique (fun n : nat => partialApply (fn n) x (x0 n))). exact c0. exact H. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete