proposition: Lemma ProdIntegrableSubsetRight_match : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)) (xyH : Domain (ProdLFunc hn) (x,y)) (init : X (ElemFunc J) -> Prop), init y -> SubsetIntersectRight hn init (ProdIntegrableSubsetRight hn x y xyH) y.
proof: Proof. induction hn. - intros. exact H. - intros. destruct xyH, d, d1; split. exact p. apply IHhn. exact H. apply IHhn. exact H. exact n. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile