fact: Record IntegralDominated {IS : IntegrationSpace} (fn : nat -> @PartialFunction (RealT (ElemFunc IS)) (X (ElemFunc IS))) (fnInt : forall n:nat, IntegrableFunction (fn n)) (eps : CRcarrier (RealT (ElemFunc IS))) : Type := { idom_support : (X (ElemFunc IS)) -> Prop; idom_idx : nat; idom_delta : CRcarrier (RealT (ElemFunc IS)); idom_delta_pos : 0 < idom_delta; idom_int : IntegrableSet idom_support; idom_dom : forall (B : X (ElemFunc IS) -> Prop) (Bmes : MeasurableSet B) (n:nat), le idom_idx n -> Integral (MeasurableIntersectIntegrable Bmes idom_int) < idom_delta -> Integral (RestrictedMeasurable (fnInt n) Bmes) < eps }.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile