fact: Definition IntegralSupport {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (A : (X (ElemFunc IS)) -> Prop) (eps : CRcarrier (RealT (ElemFunc IS))) : Type := { isupp_int : IntegrableSet A & IntegralDistance fInt (RestrictedIntegrable fInt isupp_int) < eps }.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile