fact: Definition FunctionRieszSpaceCompletion (IS : IntegrationSpace) : FunctionRieszSpace.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase