proposition: Lemma ProdLFuncApplyZero : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)) (xyS : Domain (ProdLFunc hn) (x,y)), (forall (n:nat) (ltnh : lt n (length hn)), partialApply _ _ (DomainProdLFuncInc hn x y xyS n ltnh) == 0) -> partialApply _ _ xyS == 0.
proof: Proof. induction hn. - intros. reflexivity. - intros. destruct xyS. transitivity (partialApply _ _ d + partialApply _ _ d0). reflexivity. rewrite IHhn, CRplus_0_r. clear IHhn. assert (O < length (a :: hn))%nat. { apply le_n_S, Nat.le_0_l. } rewrite <- (H O H0). apply DomainProp. clear IHhn. intros. assert (S n < length (a :: hn))%nat. { apply le_n_S, ltnh. } rewrite <- (H (S n) H0). apply DomainProp. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile