proposition: Lemma ProdLFuncDomainLeft : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)), Domain (ProdLFunc hn) (x,y) -> { n:nat | lt n (length hn) /\ prodint_f (nth n hn (ProdIntegrableZero I J)) x } + { forall n:nat, lt n (length hn) -> ~prodint_f (nth n hn (ProdIntegrableZero I J)) x }.
proof: Proof. induction hn. - intros x y H. right. intros. exfalso. inversion H0. - intros x y H. destruct H, d. unfold fst in d. destruct d. + left. exists O. split. apply le_n_S, Nat.le_0_l. exact p. + specialize (IHhn x y d0) as [[k isin] | isout]. left. exists (S k). destruct isin. split. apply le_n_S, H. exact H0. right. intros. destruct n0. exact n. apply isout. apply le_S_n, H. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile