proposition: Lemma DomainProdLFuncAppLeft : forall {I J : IntegrationSpace} (l k : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)), Domain (ProdLFunc (l ++ k)) (x,y) -> Domain (ProdLFunc l) (x, y).
proof: Proof. induction l. - intros. simpl. trivial. - intros k x y H. destruct H. split. exact d. exact (IHl k x y d0). Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile