proposition: Lemma MeasureAdditive : forall {IS : IntegrationSpace} (A B : X (ElemFunc IS) -> Prop) (aInt : IntegrableSet A) (bInt : IntegrableSet B), MeasureSet aInt + MeasureSet bInt == MeasureSet (IntegrableSetUnion A B aInt bInt) + MeasureSet (IntegrableSetIntersect A B aInt bInt).
proof: Proof. intros. setoid_replace (MeasureSet aInt + MeasureSet bInt) with (Integral (IntegrablePlus _ _ aInt bInt)). setoid_replace (MeasureSet (IntegrableSetUnion A B aInt bInt) + MeasureSet (IntegrableSetIntersect A B aInt bInt)) with (Integral (IntegrablePlus _ _ (IntegrableSetUnion A B aInt bInt) (IntegrableSetIntersect A B aInt bInt))). - apply IntegralExtensional. intros. destruct xdf,xdg; simpl. destruct d. destruct d1. 2: exfalso; apply n; left; exact a. destruct d0. destruct d2. reflexivity. exfalso; apply n; split; assumption. destruct d2. exfalso. destruct a0. contradiction. reflexivity. destruct d0, d1, d2. exfalso. apply n, a. apply CRplus_comm. reflexivity. exfalso. apply n0. right. exact b. exfalso. apply n, a. exfalso. destruct o; contradiction. exfalso. apply n, a. reflexivity. - rewrite IntegralPlus. reflexivity. - rewrite IntegralPlus. reflexivity. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity