Nuprl Definition : infinite-deriv-seq
infinite-deriv-seq(I;i,x.F[i; x]) ==  ∀i:ℕ. λx.F[i + 1; x] = d(F[i; x])/dx on I
Definitions occuring in Statement : 
derivative: λz.g[z] = d(f[x])/dx on I
, 
nat: ℕ
, 
all: ∀x:A. B[x]
, 
add: n + m
, 
natural_number: $n
Definitions occuring in definition : 
all: ∀x:A. B[x]
, 
nat: ℕ
, 
derivative: λz.g[z] = d(f[x])/dx on I
, 
add: n + m
, 
natural_number: $n
FDL editor aliases : 
infinite-deriv-seq
Latex:
infinite-deriv-seq(I;i,x.F[i;  x])  ==    \mforall{}i:\mBbbN{}.  \mlambda{}x.F[i  +  1;  x]  =  d(F[i;  x])/dx  on  I
Date html generated:
2016_05_18-AM-10_28_03
Last ObjectModification:
2015_09_23-AM-09_16_00
Theory : reals
Home
Index