proposition: Lemma MeasurableSetUnion : 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 _]. apply (IntegrableFunctionExtensional (Xminus (Xplus (Xmult (CharacFunc A) (CharacFunc C)) (Xmult (CharacFunc B) (CharacFunc C))) (Xmult (CharacFunc A) (CharacFunc (fun x => B x /\ C x))))). - split. + intros x. simpl. intros. destruct H, p, p. split. 2: exact s0. destruct s. left. left. exact a. destruct p1, s. left. right. exact b. right. intro abs. destruct abs; contradiction. + intros. destruct xD. rewrite (applyXminus (Xplus (Xmult (CharacFunc A) (CharacFunc C)) (Xmult (CharacFunc B) (CharacFunc C))) (Xmult (CharacFunc A) (CharacFunc (fun x0 : X (ElemFunc IS) => B x0 /\ C x0))) x d d0). destruct d. rewrite (applyXplus _ _ x d d1). destruct d. rewrite (applyXmult _ _ x d d2). destruct d1. rewrite (applyXmult _ _ x d1 d3). rewrite (DomainProp _ x d3 d2). clear d3. destruct d0. rewrite (applyXmult _ _ x d0 d3). rewrite (DomainProp _ x d0 d). clear d0. destruct xG. rewrite (applyXmult _ _ x d0 d4). rewrite (DomainProp _ x d4 d2). clear d4. simpl. destruct d2. rewrite CRmult_1_r, CRmult_1_r, CRmult_1_r. destruct d1. destruct d3. destruct d. destruct d0. rewrite CRmult_1_r. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_r. apply CRplus_0_r. contradict n. left. exact a0. destruct d0. rewrite CRmult_0_l, CRplus_0_l. unfold CRminus. rewrite CRopp_0, CRplus_0_r. reflexivity. contradict n0. right. exact b. contradict n. split; assumption. destruct d3. destruct a; contradiction. rewrite CRmult_0_r. destruct d. destruct d0. rewrite CRplus_0_r. unfold CRminus. rewrite CRopp_0, CRplus_0_r. reflexivity. contradict n1. left. exact a. destruct d0. destruct o; contradiction. rewrite CRplus_0_l. apply CRplus_opp_r. destruct d3. destruct a. contradiction. rewrite CRmult_0_r, CRmult_0_r, CRmult_0_r, CRplus_0_l. apply CRplus_opp_r. - apply IntegrableMinus. apply IntegrablePlus. apply (Aint Ameas), Cint. apply (Bint Bmeas), Cint. apply (Aint Ameas). exact (MeasurableIntersectIntegrable Bmeas Cint). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile