Nuprl Definition : case-real
case-real(a;b;f) == accelerate(3;λn.if 4 <z |(a n) - b n| ∧b (f n) then a n else b n fi )
Definitions occuring in Statement :
accelerate: accelerate(k;f),
band: p ∧b q,
absval: |i|,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
apply: f a,
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
accelerate: accelerate(k;f),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
band: p ∧b q,
lt_int: i <z j,
natural_number: $n,
absval: |i|,
subtract: n - m,
apply: f a
FDL editor aliases :
case-real
Latex:
case-real(a;b;f) == accelerate(3;\mlambda{}n.if 4 <z |(a n) - b n| \mwedge{}\msubb{} (f n) then a n else b n fi )
Date html generated:
2019_10_29-AM-09_36_30
Last ObjectModification:
2019_05_23-PM-03_41_31
Theory : reals
Home
Index