fact: Definition InverseImageIntegrableGivenLimit {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (t : CRcarrier (RealT (ElemFunc IS))) (tPos : 0 < t) : CR_cauchy _ (fun n:nat => Integral (StepApproxIntegrable f _ t (StepApproxBetween t tPos n) fInt)) -> { limInt : IntegrableSet (fun x => exists xD:Domain f x, t <= partialApply f x xD) & CR_cv _ (fun n:nat => Integral (StepApproxIntegrable f _ t (StepApproxBetween t tPos n) fInt)) (MeasureSet limInt) }.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia