proposition: Lemma MeasurableConst : forall {IS : IntegrationSpace} (a : CRcarrier (RealT (ElemFunc IS))), MeasurableFunction (Xconst (X (ElemFunc IS)) a).
proof: Proof. intros IS a A k Aint. apply IntegrableMaxConst. apply IntegrableMinConst. apply (IntegrableFunctionExtensional (Xscale a (CharacFunc A))). - split. intros x xdf. split. exact xdf. simpl. trivial. intros. simpl. destruct xG. destruct xD. destruct d. apply CRmult_comm. contradiction. destruct d. contradiction. apply CRmult_comm. - apply IntegrableScale, Aint. - apply CR_of_Q_lt. reflexivity. - apply CR_of_Q_lt. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile