proposition: Lemma MeasurableSetIntersection : forall {IS : IntegrationSpace} (A B : (X (ElemFunc IS)) -> Prop), MeasurableSet A -> MeasurableSet B -> MeasurableSet (fun x => A x /\ B x).
proof: Proof. intros IS A B Ameas Bmeas. apply MeasurableSetEquiv. intros C Cint. pose proof (MeasurableSetEquiv A) as [Aint _]. pose proof (MeasurableSetEquiv B) as [Bint _]. pose proof (MeasurableFunctionFull _ Bmeas) as Bfull. specialize (Aint Ameas). specialize (Bint Bmeas). apply (IntegrableExtensionalAE (Xmult (CharacFunc A) (CharacFunc (fun x => B x /\ C x)))). - destruct Bfull. exists (Xplus x (Xmult (CharacFunc A) (CharacFunc C))). split. apply IntegrablePlus. apply p. apply Aint. exact Cint. intros. destruct p, H, d1. specialize (d x0 d0). split. 2: exact d2. simpl. destruct d1. destruct d. 2: right; intros [H1 H0]; contradiction. left. split; assumption. right. intros [H H0]. contradiction. - exists (CharacFunc C). split. exact Cint. intros. simpl. destruct dF, dG. clear H. destruct d2. destruct d0. destruct d1. destruct d. reflexivity. destruct a0; contradiction. destruct d. contradict n. split. exact a0. apply a. reflexivity. rewrite CRmult_0_r. destruct d1. contradict n. split. apply a. exact c. rewrite CRmult_0_l. reflexivity. rewrite CRmult_0_r. destruct d0. destruct a; contradiction. apply CRmult_0_r. - apply Aint. apply (IntegrableFunctionExtensional (Xmult (CharacFunc B) (CharacFunc C))). split. intros x xdf. destruct xdf. destruct d. destruct d0. left. split; assumption. right. intro abs. destruct abs. contradiction. right. intro abs. destruct abs. contradiction. intros. 2: apply Bint; assumption. simpl. destruct xD. destruct d. destruct d0. destruct xG. apply CRmult_1_l. contradict n. split; assumption. destruct xG. destruct a; contradiction. apply CRmult_0_r. rewrite CRmult_0_l. destruct xG. destruct a; contradiction. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile