proposition: Lemma MeasureEmptyZero : forall {IS : IntegrationSpace} (A : X (ElemFunc IS) -> Prop) (aInt : IntegrableSet A), (forall x:X (ElemFunc IS), { A x } + { ~A x } -> ~A x) -> MeasureSet aInt == 0.
proof: Proof. intros. transitivity (Integral (@IntegrableZero IS)). apply IntegralExtensional. intros. simpl. destruct xdf. 2: reflexivity. exfalso. specialize (H x (left a)). contradiction. apply IntegralZeroIsZero. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity