fact: Definition IElemProduct { I J : IntegrationSpace } (f : PartialFunction (prod (X (ElemFunc I)) (X (ElemFunc J)))) : L (ProductFunctionRieszSpace I J) f -> CRcarrier (RealT (ElemFunc I)) := fun fL => let (l,_) := fL in fold_right (CRplus (RealT (ElemFunc I))) 0 (map (fun pi => prodint_factor pi * MeasureSet (prodint_fint pi) * CRcast (MeasureSet (prodint_gint pi))) l).
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile