proposition: Lemma MeasurableFunctionExtensional : forall {IS : IntegrationSpace} (f g : PartialFunction (X (ElemFunc IS))), PartialRestriction f g -> MeasurableFunction f -> MeasurableFunction g.
proof: Proof. intros IS f g [d c] fMes A k Aint. apply (IntegrableFunctionExtensional (XmaxConst (XminConst (Xmult (CharacFunc A) f) (CR_of_Q (RealT (ElemFunc IS)) (Z.pos k # 1))) (CR_of_Q (RealT (ElemFunc IS)) (Z.neg k # 1)))). 2: exact (fMes A k Aint). split. - intros x xdf. simpl in xdf. destruct xdf. split. exact s. exact (d x d0). - intros. simpl. destruct xD, xG. rewrite (c x d1 (d x d1)), (DomainProp g x (d x d1) d3). destruct d0. destruct d2. reflexivity. contradiction. destruct d2. contradiction. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile