proposition: Lemma MeasureIntersectSym : forall {IS : IntegrationSpace} (A B : X (ElemFunc IS) -> Prop) (aInt : IntegrableSet A) (bInt : IntegrableSet B), MeasureSet (IntegrableSetIntersect A B aInt bInt) == MeasureSet (IntegrableSetIntersect B A bInt aInt).
proof: Proof. intros. unfold MeasureSet. apply IntegralExtensional. intros. destruct xdf,xdg; simpl. reflexivity. exfalso. apply n. split; apply a. exfalso. apply n. split; apply a. reflexivity. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity