proposition: Lemma InverseImageIntegrableAE : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f), { s : nat -> CRcarrier (RealT (ElemFunc IS)) & forall t (tPos : 0 < t), (forall n:nat, CRapart _ t (s n)) -> { 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) } }.
proof: Proof. intros. destruct (FindJumpPointsCountable f fInt). exists x. intros. apply (InverseImageIntegrableGivenLimit f fInt t tPos). apply StepApproxBoundCv. apply (s t tPos H). Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia