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