Nuprl Definition : baire-diff-from

baire-diff-from(a;k) ==  λn.if k ≤z n then if a k=a k-1  then (a k-1) + 1  else (a k-1) else a n fi 


Definitions occuring in Statement :  nat-pred: n-1,  le_int: i ≤z j,  ifthenelse: if b then t else f fi ,  int_eq: if a=b  then c  else d,  apply: f a,  lambda: λx.A[x],  add: n + m,  natural_number: $n
Definitions occuring in definition :  apply: f a,  nat-pred: n-1,  natural_number: $n,  add: n + m,  int_eq: if a=b  then c  else d,  le_int: i ≤z j,  ifthenelse: if b then t else f fi ,  lambda: λx.A[x]
FDL editor aliases :  baire-diff-from
Latex:
baire-diff-from(a;k)  ==    \mlambda{}n.if  k  \mleq{}z  n  then  if  a  k=a  k-1    then  (a  k-1)  +  1    else  (a  k-1)  else  a  n  fi 


Date html generated: 2017_04_21-AM-11_23_29
Last ObjectModification: 2017_04_20-PM-05_44_39

Theory : continuity


Home Index