fact: Definition IntegrableMinConst {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (a : CRcarrier _) : IntegrableFunction f -> 0 < a -> IntegrableFunction (XminConst f a) := fun fInt aPos => @LminConstStable (FunctionRieszSpaceCompletion IS) a f aPos fInt.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase