proposition: Lemma MeasureIntersectIncr : forall {IS : IntegrationSpace} (A B : X (ElemFunc IS) -> Prop) (aInt : IntegrableSet A) (bInt : IntegrableSet B), MeasureSet (IntegrableSetIntersect A B aInt bInt) <= MeasureSet bInt.
proof: Proof. intros. apply MeasureNonDecreasing. intros. apply H. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity