fact: Definition TotalizeFunc {R : ConstructiveReals} (X : Set) (f : PartialFunction X) (domainTotal : forall x:X, Domain f x) : X -> CRcarrier R := fun x => partialApply f x (domainTotal x).
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete