fact: Definition ProdIntegrableSimplify {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) : list (@ProdIntegrable I J) := map (fun xy => ProdSubsetIntersect hn (fst xy) (snd xy)) (list_prod (FreeSubsets (length hn)) (FreeSubsets (length hn))).
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile