Nuprl Definition : enum-fin-seq-max2
enum-fin-seq-max2(M;m) == imax-list(map(λs.case M m s of inl(k) => k + 1 | inr(x) => 0;enum-fin-seq(m)))
Definitions occuring in Statement :
enum-fin-seq: enum-fin-seq(m),
imax-list: imax-list(L),
map: map(f;as),
apply: f a,
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
add: n + m,
natural_number: $n
Definitions occuring in definition :
imax-list: imax-list(L),
map: map(f;as),
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
apply: f a,
add: n + m,
natural_number: $n,
enum-fin-seq: enum-fin-seq(m)
FDL editor aliases :
enum-fin-seq-max2
Latex:
enum-fin-seq-max2(M;m) ==
imax-list(map(\mlambda{}s.case M m s of inl(k) => k + 1 | inr(x) => 0;enum-fin-seq(m)))
Date html generated:
2016_05_14-PM-09_46_48
Last ObjectModification:
2015_10_22-AM-08_40_15
Theory : continuity
Home
Index