fact: Definition IntegrableFunction {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) : Type := { fInt : IntegralRepresentation & PartialRestriction (XinfiniteSumAbs (IntFn fInt)) f }.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase