proposition: Lemma DomainProdLFuncIncReverse : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)), (forall n:nat, lt n (length hn) -> Domain (ProdIntegrableFunc (nth n hn (ProdIntegrableZero I J))) (x,y)) -> Domain (ProdLFunc hn) (x,y).
proof: Proof. induction hn. - intros. simpl. trivial. - intros x y H. split. + apply (H O). apply le_n_S, Nat.le_0_l. + apply IHhn. intros. apply le_n_S in H0. exact (H (S n) H0). Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile