Nuprl Definition : find-real-neq

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


Definitions occuring in Statement :  mu-ge-print: mu-ge-print(f;n),  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 :  mu-ge-print: mu-ge-print(f;n),  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-neq
Latex:
find-real-neq(a;b)  ==
    eval  x  =  a  in
    eval  y  =  b  in
        mu-ge-print(\mlambda{}n.eval  xn  =  x  n  in
                                      eval  yn  =  y  n  in
                                      eval  d  =  xn  -  yn  in
                                          1  <z  |d|;0)


Date html generated: 2016_05_18-AM-09_35_23
Last ObjectModification: 2015_09_23-AM-09_11_46

Theory : reals


Home Index