proposition: Lemma partialInfiniteTriangle : forall {R : ConstructiveReals} (X : Set) (fn : nat -> @PartialFunction R X) (x : X) (xD : Domain (XinfiniteSumAbs fn) x), CRle _ (CRabs _ (partialApply _ x xD)) (let (xn, cv) := xD in let (l,_) := CR_complete R _ cv in l).
proof: Proof. intros. destruct xD as [xn limAbs]; simpl. destruct (series_cv_abs (fun n : nat => partialApply (fn n) x (xn n)) limAbs). apply (series_cv_triangle (fun k : nat => partialApply (fn k) x (xn k))). exact s. destruct (CR_complete R (CRsum (fun n : nat => CRabs _ (partialApply (fn n) x (xn n)))) limAbs). exact c. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions