Nuprl Definition : uniform-continuity-pi-search

uniform-continuity-pi-search(G;n;x)
==r if n ≤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 ≤then n
                                       if isl(G x) then x
                                       else uniform-continuity-pi-search (x 1)
                                       fi )) 
  x



Definitions occuring in Statement :  le_int: i ≤j ifthenelse: if then else fi  isl: isl(x) apply: a fix: fix(F) lambda: λx.A[x] add: m natural_number: $n
Definitions occuring in definition :  fix: fix(F) lambda: λx.A[x] le_int: i ≤j ifthenelse: if then else fi  isl: isl(x) apply: a add: 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