proposition: Lemma MeasurableSetCompl : forall {IS : IntegrationSpace} (A : (X (ElemFunc IS)) -> Prop), MeasurableSet A -> MeasurableSet (fun x => ~A x).
proof: Proof. intros IS A Ameas. apply MeasurableSetEquiv. intros B Bint. destruct (MeasurableSetEquiv A) as [H _]. specialize (H Ameas B Bint). refine (IntegrableFunctionExtensional _ _ _ (IntegrableMinus Bint H)). split. - intros x. simpl. intros. destruct H0, p. split. destruct s0. right. intro abs. contradiction. left. exact n. exact s. - intros. destruct xD, d. + simpl. destruct d0. destruct d0. 2: contradiction. destruct xG. destruct d1. 2: contradiction. destruct d. destruct d0. contradiction. rewrite CRmult_1_r, CRmult_1_r, CRmult_1_r. apply CRplus_opp_r. destruct d0. 2: contradiction. rewrite CRmult_0_l, CRmult_0_r. rewrite CRmult_1_l, CRplus_0_r. reflexivity. + simpl. destruct xG. destruct d0. destruct d2. contradiction. destruct d1. contradiction. rewrite CRmult_0_r, CRmult_0_r, CRmult_0_r. apply CRplus_0_l. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile