fact: Definition SubsetIntersectLeft {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) (init : X (ElemFunc I) -> Prop) (filter : list bool) : X (ElemFunc I) -> Prop := SubsetIntersectFilter (map prodint_f hn) init filter.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile