Nuprl Definition : uniform-continuity-pi-search

uniform-continuity-pi-search(G;n;x)
==r if n ≤z x then n
    if isl(G x) then x
    else uniform-continuity-pi-search(G;n;x + 1)
    fi 
uniform-continuity-pi-search(G;n;x) ==
  fix((λuniform-continuity-pi-search,x. if n ≤z x then n
                                       if isl(G x) then x
                                       else uniform-continuity-pi-search (x + 1)
                                       fi )) 
  x


Definitions occuring in Statement :  le_int: i ≤z j,  ifthenelse: if b then t else f fi ,  isl: isl(x),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  le_int: i ≤z j,  ifthenelse: if b then t else f fi ,  isl: isl(x),  apply: f a,  add: n + m,  natural_number: $n
FDL editor aliases :  uniform-continuity-pi-search
Latex:
uniform-continuity-pi-search(G;n;x)
==r  if  n  \mleq{}z  x  then  n
        if  isl(G  x)  then  x
        else  uniform-continuity-pi-search(G;n;x  +  1)
        fi 

Latex:
uniform-continuity-pi-search(G;n;x)  ==
    fix((\mlambda{}uniform-continuity-pi-search,x.  if  n  \mleq{}z  x  then  n
                                                                              if  isl(G  x)  then  x
                                                                              else  uniform-continuity-pi-search  (x  +  1)
                                                                              fi  )) 
    x


Date html generated: 2016_05_14-PM-09_39_04
Last ObjectModification: 2015_09_22-PM-06_03_35

Theory : continuity


Home Index