fact: Definition StepApproxBound {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (t1 t2 b : CRcarrier (RealT (ElemFunc IS))) (let1t2 : t1 <= t2) : Set := { ext : @IntervalExtension _ t1 t2 & Integral (StepApproxIntegrable f (t1 - ext_eta ext) t1 (left_ordered ext) fInt) - Integral (StepApproxIntegrable f t2 (t2 + ext_eta ext) (pair (IntExtRightPos ext let1t2) (right_ordered ext)) fInt) < b }.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia