proposition: Lemma IntegrableMeasurable : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))), IntegrableFunction f -> MeasurableFunction f.
proof: Proof. intros IS f fInt A k Aint. apply IntegrableMaxConst. apply IntegrableMinConst. exact (RestrictedIntegrable fInt Aint). apply CR_of_Q_pos. reflexivity. apply (CRlt_le_trans _ (CR_of_Q _ 0)). apply CR_of_Q_lt. reflexivity. apply CRle_refl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile