Nuprl Definition : find-real-neq2

find-real-neq2(a;b) ==
  eval x = a in
  eval y = b in
    find-xover-print(λn.eval xn = x n in
                        eval yn = y n in
                        eval d = xn - yn in
                          1 <z |d|;0;0;1)


Definitions occuring in Statement :  find-xover-print: find-xover-print(f;m;n;step),  absval: |i|,  callbyvalue: callbyvalue,  lt_int: i <z j,  apply: f a,  lambda: λx.A[x],  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  find-xover-print: find-xover-print(f;m;n;step),  lambda: λx.A[x],  apply: f a,  callbyvalue: callbyvalue,  subtract: n - m,  lt_int: i <z j,  absval: |i|,  natural_number: $n
FDL editor aliases :  find-real-neq2
Latex:
find-real-neq2(a;b)  ==
    eval  x  =  a  in
    eval  y  =  b  in
        find-xover-print(\mlambda{}n.eval  xn  =  x  n  in
                                                eval  yn  =  y  n  in
                                                eval  d  =  xn  -  yn  in
                                                    1  <z  |d|;0;0;1)


Date html generated: 2016_05_18-AM-09_35_36
Last ObjectModification: 2015_09_23-AM-09_11_55

Theory : reals


Home Index