Nuprl Definition : extl2Cantor
extl2Cantor(s;b) ==  λx.if x <z ||s|| then s[x] else b fi 
Definitions occuring in Statement : 
select: L[n]
, 
length: ||as||
, 
ifthenelse: if b then t else f fi 
, 
lt_int: i <z j
, 
lambda: λx.A[x]
Definitions occuring in definition : 
lambda: λx.A[x]
, 
ifthenelse: if b then t else f fi 
, 
lt_int: i <z j
, 
length: ||as||
, 
select: L[n]
FDL editor aliases : 
extl2Cantor
Latex:
extl2Cantor(s;b)  ==    \mlambda{}x.if  x  <z  ||s||  then  s[x]  else  b  fi 
Date html generated:
2016_05_14-PM-09_38_13
Last ObjectModification:
2015_09_22-PM-06_03_33
Theory : continuity
Home
Index