proposition: Lemma IntegrableMeasurableSet : forall {IS : IntegrationSpace} (A : X (ElemFunc IS) -> Prop), IntegrableSet A -> MeasurableSet A.
proof: Proof. intros IS A Aint B k Bint. apply IntegrableMaxConst. apply IntegrableMinConst. apply (IntegrableExtensionalAE (CharacFunc (fun x => B x /\ A x))). - exists (Xplus (CharacFunc A) (CharacFunc B)). split. exact (IntegrablePlus _ _ Aint Bint). intros. split. apply H. apply H. - exists (CharacFunc A). split. exact Aint. intros. simpl. destruct dG. clear H. destruct d0. + rewrite CRmult_1_r. destruct d, dF. reflexivity. contradict n. split; assumption. destruct a0. contradiction. reflexivity. + rewrite CRmult_0_r. destruct dF. destruct a. contradiction. reflexivity. - exact (IntegrableSetIntersect _ _ Bint 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