Nuprl Definition : cover-real

cover-real(d; a; b; cb) ==  accelerate(2;λn.((fst(cover-seq(d;a;b;log(2;n * (cb + 1))))) n))


Definitions occuring in Statement :  cover-seq: cover-seq(d;a;b;n),  accelerate: accelerate(k;f),  log: log(b;n),  pi1: fst(t),  apply: f a,  lambda: λx.A[x],  multiply: n * m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  accelerate: accelerate(k;f),  lambda: λx.A[x],  apply: f a,  pi1: fst(t),  cover-seq: cover-seq(d;a;b;n),  log: log(b;n),  multiply: n * m,  add: n + m,  natural_number: $n
Latex:
cover-real(d;  a;  b;  cb)  ==    accelerate(2;\mlambda{}n.((fst(cover-seq(d;a;b;log(2;n  *  (cb  +  1)))))  n))


Date html generated: 2019_10_30-AM-07_18_57
Last ObjectModification: 2019_04_03-PM-08_23_54

Theory : reals


Home Index