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