fact: Definition StepApprox {R : ConstructiveReals} {X : Set} (f : PartialFunction X) (s t : CRcarrier R) (ltst : s < t) : PartialFunction X := Xscale (CRinv R (t - s) (inr (CRlt_minus s t ltst))) (Xminus (XminConst f t) (XminConst f s)).
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia