proposition: Lemma MeasurableIntegrableSubset : forall {IS : IntegrationSpace} (A B : X (ElemFunc IS) -> Prop), IntegrableSet B -> MeasurableSet A -> (forall x : X (ElemFunc IS), A x -> B x) -> IntegrableSet A.
proof: Proof. intros IS A B Bint Ames incl. specialize (Ames B 1%positive Bint). refine (IntegrableFunctionExtensional _ _ _ Ames). split. - intros x xdf. exact (snd xdf). - intros. destruct xG. + simpl. destruct xD. destruct d. 2: contradict n; exact (incl x a). destruct d0. rewrite CRmult_1_l, CRmin_left, CRmax_left. reflexivity. apply CR_of_Q_le. discriminate. apply CRle_refl. contradiction. + simpl. destruct xD. destruct d0. contradiction. rewrite CRmult_0_r, CRmin_left, CRmax_left. reflexivity. apply CR_of_Q_le. discriminate. apply CR_of_Q_le. discriminate. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile