Nuprl Definition : finite-deriv-seq
finite-deriv-seq(I;k;i,x.F[i; x]) == ∀i:ℕk. λ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,
int_seg: {i..j-},
all: ∀x:A. B[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
int_seg: {i..j-},
derivative: λz.g[z] = d(f[x])/dx on I,
add: n + m,
natural_number: $n
FDL editor aliases :
finite-deriv-seq
Latex:
finite-deriv-seq(I;k;i,x.F[i; x]) == \mforall{}i:\mBbbN{}k. \mlambda{}x.F[i + 1; x] = d(F[i; x])/dx on I
Date html generated:
2016_05_18-AM-10_20_20
Last ObjectModification:
2015_09_23-AM-09_15_49
Theory : reals
Home
Index