Nuprl Definition : case-real2
case-real2(a;b;f) == case-real(a;b;λn.if (a n) + 4 <z b n then f (inl n) else f (inr n ) fi )
Definitions occuring in Statement :
case-real: case-real(a;b;f),
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
apply: f a,
lambda: λx.A[x],
inr: inr x ,
inl: inl x,
add: n + m,
natural_number: $n
Definitions occuring in definition :
case-real: case-real(a;b;f),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
add: n + m,
natural_number: $n,
inl: inl x,
apply: f a,
inr: inr x
FDL editor aliases :
case-real2
Latex:
case-real2(a;b;f) == case-real(a;b;\mlambda{}n.if (a n) + 4 <z b n then f (inl n) else f (inr n ) fi )
Date html generated:
2019_10_29-AM-09_36_51
Last ObjectModification:
2019_05_23-PM-05_46_43
Theory : reals
Home
Index