fact: Definition StepApproxIntegrable {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (s t : CRcarrier (RealT (ElemFunc IS))) (ltst : 0 < s < t) : IntegrableFunction f -> IntegrableFunction (StepApprox f s t (snd ltst)) := fun fInt => IntegrableScale _ _ (IntegrableMinus (IntegrableMinConst f t fInt (CRlt_trans 0 s t (fst ltst) (snd ltst))) (IntegrableMinConst f s fInt (fst ltst))).
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia