proposition: Lemma SubsetIntersectRightIntegrable : forall {I J : IntegrationSpace} (subset : list bool) (init : X (ElemFunc J) -> Prop) (hn : list (@ProdIntegrable I J)), IntegrableSet init -> IntegrableSet (SubsetIntersectRight hn init subset).
proof: Proof. induction subset as [|a subset]. - intros init hn initInt. destruct hn; exact initInt. - intros. simpl. destruct hn as [|p hn]. exact X. destruct a. apply IntegrableSetIntersect. apply p. apply IHsubset. exact X. apply IntegrableSetDifference. apply IHsubset. exact X. apply p. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile