proposition: Lemma IntegrableSetAEdecidable : forall {IS : IntegrationSpace} (A : (X (ElemFunc IS)) -> Prop) (f : @PartialFunctionXY (X (ElemFunc IS)) bool eq), IntegrableFunction (PartialFunctionBoolR f) -> (forall (x : X (ElemFunc IS)) (dec : Domain f x), if partialApply f x dec then A x else ~A x) -> IntegrableSet A.
proof: Proof. intros IS A f fInt. destruct fInt. exists x. apply (PartialRestriction_trans _ _ (PartialFunctionBoolR f) _ p). split. - intros y yD. simpl in yD. specialize (H y yD). destruct (partialApply f y yD). left. exact H. right. exact H. - intros. simpl. specialize (H x0 xD). destruct (partialApply f x0 xD), xG. reflexivity. 3: reflexivity. contradiction. contradiction. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity