Nuprl Definition : cantor2baire-aux
cantor2baire-aux(a;n) == primrec(n;0;λm,r. if a (m + 1) then r + 1 else r fi )
Definitions occuring in Statement :
primrec: primrec(n;b;c),
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
add: n + m,
apply: f a,
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
primrec: primrec(n;b;c)
FDL editor aliases :
cantor2baire-aux
Latex:
cantor2baire-aux(a;n) == primrec(n;0;\mlambda{}m,r. if a (m + 1) then r + 1 else r fi )
Date html generated:
2017_04_21-AM-11_21_30
Last ObjectModification:
2017_04_20-PM-03_37_37
Theory : continuity
Home
Index