fact: Definition IntegrableSet {IS : IntegrationSpace} (A : (X (ElemFunc IS)) -> Prop) : Type := IntegrableFunction (CharacFunc A).
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity