proposition: Lemma applyInfiniteSumAbs : forall {R : ConstructiveReals} (X : Set) (fn : nat -> PartialFunction X) (x : X) (xD : Domain (XinfiniteSumAbs fn) x) (a : CRcarrier R), prod (partialApply (XinfiniteSumAbs fn) x xD == a -> series_cv (fun n => partialApply (fn n) x (domainInfiniteSumAbsIncReverse fn x xD n)) a) (series_cv (fun n => partialApply (fn n) x (domainInfiniteSumAbsIncReverse fn x xD n)) a -> partialApply (XinfiniteSumAbs fn) x xD == a).
proof: Proof. intros. unfold domainInfiniteSumAbsIncReverse. destruct xD. simpl. destruct (series_cv_abs (fun n : nat => partialApply (fn n) x (x0 n))). split. - intros. exact (CR_cv_proper _ _ _ s H). - intros. apply (series_cv_unique (fun n : nat => partialApply (fn n) x (x0 n))); assumption. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete