fact: Definition domainInfiniteSumAbsScaleInc {R : ConstructiveReals} (X : Set) (fn : nat -> @PartialFunction R X) (a : CRcarrier R) (x : X) (xD : Domain (XinfiniteSumAbs fn) x) : { y : Domain (XinfiniteSumAbs (fun n : nat => Xscale a (fn n))) x | partialApply _ x y == (partialApply _ x xD) * a }.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase