proposition: Lemma MeasurableIntersectIntegrable : forall {IS : IntegrationSpace} {A B : (X (ElemFunc IS)) -> Prop}, MeasurableSet A -> IntegrableSet B -> IntegrableSet (fun x => A x /\ B x).
proof: Proof. intros IS A B Ames Bint. pose proof (MeasurableSetEquiv A) as [Aint _]. specialize (Aint Ames B Bint). refine (IntegrableFunctionExtensional _ _ _ Aint). split. - intros x [d d0]. destruct d, d0. left. split; assumption. right. intros [_ abs]. contradiction. right. intros [abs _]. contradiction. right. intros [abs _]. contradiction. - intros. simpl. destruct xD. destruct d. destruct xG. destruct d0. apply CRmult_1_r. destruct a0; contradiction. destruct d0. contradict n. split; assumption. 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