fact: Definition MeasurableMonotoneConvergenceClassical {IS : IntegrationSpace} (fn : nat -> PartialFunction (X (ElemFunc IS))) : (forall n:nat, MeasurableFunction (fn n)) -> (forall n:nat, partialFuncLe (fn n) (fn (S n))) -> IncrSeqCvT -> (forall x : X (ElemFunc IS), Domain (XpointwiseLimit fn) x) -> MeasurableFunction (XpointwiseLimit fn).
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile