fact: Definition StepApproxBoundOpen {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (t1 t2 b : CRcarrier (RealT (ElemFunc IS))) : Prop := forall x y u v (ltxy : 0 < x < y) (ltuv : 0 < u < v), t1 < x -> y <= u -> v < t2 -> Integral (StepApproxIntegrable f x y ltxy fInt) - Integral (StepApproxIntegrable f u v ltuv fInt) <= b.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia