Nuprl Definition : baire2cantor
baire2cantor(a) == λn.if (a n =z a n-1) then ff else tt fi
Definitions occuring in Statement :
nat-pred: n-1,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
bfalse: ff,
btrue: tt,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
btrue: tt,
bfalse: ff,
nat-pred: n-1,
apply: f a,
eq_int: (i =z j),
ifthenelse: if b then t else f fi ,
lambda: λx.A[x]
FDL editor aliases :
baire2cantor
Latex:
baire2cantor(a) == \mlambda{}n.if (a n =\msubz{} a n-1) then ff else tt fi
Date html generated:
2017_04_21-AM-11_21_19
Last ObjectModification:
2017_04_20-PM-03_36_50
Theory : continuity
Home
Index