Nuprl Definition : choose

choose(n;i) ==  Y (λchoose,n,i. if (i =z 0) ∨b(i =z n) then 1 else (choose (n - 1) (i - 1)) + (choose (n - 1) i) fi ) n \000Ci


Definitions occuring in Statement :  bor: p ∨bq,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  ycomb: Y,  apply: f a,  lambda: λx.A[x],  subtract: n - m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  ycomb: Y,  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  bor: p ∨bq,  eq_int: (i =z j),  add: n + m,  apply: f a,  subtract: n - m,  natural_number: $n
Latex:
choose(n;i)  ==
    Y 
    (\mlambda{}choose,n,i.  if  (i  =\msubz{}  0)  \mvee{}\msubb{}(i  =\msubz{}  n)  then  1  else  (choose  (n  -  1)  (i  -  1))  +  (choose  (n  -  1)  i)  fi  \000C) 
    n 
    i


Date html generated: 2016_05_15-PM-00_26_28
Last ObjectModification: 2015_09_23-AM-06_26_07

Theory : rings_1


Home Index