fact: Definition Un_integral_cv { IS : IntegrationSpace } (fn : nat -> PartialFunction (X (ElemFunc IS))) (f : PartialFunction (X (ElemFunc IS))) (fnInt : forall n:nat, IntegrableFunction (fn n)) (fInt : IntegrableFunction f) := forall p : positive, { n : nat | forall i:nat, le n i -> IntegralDistance (fnInt i) fInt <= CR_of_Q _ (1#p) }.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase