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