fact: Definition IntegrableSelf { IS : IntegrationSpace } (fInt : @IntegralRepresentation IS) : IntegrableFunction (XinfiniteSumAbs (IntFn fInt)).
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase