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