Nuprl Definition : gamma-neighbourhood
gamma-neighbourhood(beta;n0) ==
λn.if init-seg-nat-seq(n;n0) then inr ⋅
if TERMOF{extend-seq1-all-dec:o, 1:l} n n0 beta then inl 1
else inl 0
fi
Definitions occuring in Statement :
init-seg-nat-seq: init-seg-nat-seq(f;g),
ifthenelse: if b then t else f fi ,
it: ⋅,
apply: f a,
lambda: λx.A[x],
inr: inr x ,
inl: inl x,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
init-seg-nat-seq: init-seg-nat-seq(f;g),
inr: inr x ,
it: ⋅,
ifthenelse: if b then t else f fi ,
apply: f a,
extend-seq1-all-dec,
inl: inl x,
natural_number: $n
TermOfs occuring in Definition :
extend-seq1-all-dec
FDL editor aliases :
gamma-neighbourhood
Latex:
gamma-neighbourhood(beta;n0) ==
\mlambda{}n.if init-seg-nat-seq(n;n0) then inr \mcdot{}
if TERMOF\{extend-seq1-all-dec:o, 1:l\} n n0 beta then inl 1
else inl 0
fi
Date html generated:
2016_05_14-PM-09_56_19
Last ObjectModification:
2016_01_16-AM-07_55_12
Theory : continuity
Home
Index