fact: Definition Iabs {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fL : L (ElemFunc IS) f) := I IS (Xabs f) (LabsStable _ f fL).
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions