proposition: Lemma ProductMinConstStable : forall {I J : IntegrationSpace} (l : list (@ProdIntegrable I J)) (a : CRcarrier (RealT (ElemFunc I))) (aPos : 0 < a), PartialRestriction (ProdLFunc (map (ProdIntegrableMapCoef (fun x => CRmin x a)) (ProdIntegrableSimplify l))) (XminConst (ProdLFunc l) a).
proof: Proof. intros I J l. split. - intros [x y] H. apply DomainProdLFuncMap, ProdIntegrableSimplifyDomain in H. exact H. - intros [x y] xyDS xG. simpl. rewrite (ApplyProdLFuncDisjointAbs _ x y (DomainProdLFuncMap (ProdIntegrableSimplify l) x y (fun x => CRmin x a) xyDS)). 2: apply ProdIntegrableSimplifyDisjoint. apply CRmin_morph. rewrite <- (ProdIntegrableSimplifyEq l x y (ProdIntegrableSimplifyDomain l x y (DomainProdLFuncMap (ProdIntegrableSimplify l) x y (fun x => CRmin x a) xyDS))). apply DomainProp. reflexivity. rewrite CRmin_left. reflexivity. apply CRlt_asym, aPos. intros. rewrite H. reflexivity. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile