Nuprl Definition : two-factorizations
two-factorizations(n) == mapfilter(λa.<a, n ÷ a>;λa.(n rem a =z 0);[1, n + 1))
Definitions occuring in Statement :
from-upto: [n, m),
mapfilter: mapfilter(f;P;L),
eq_int: (i =z j),
lambda: λx.A[x],
pair: <a, b>,
remainder: n rem m,
divide: n ÷ m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
mapfilter: mapfilter(f;P;L),
pair: <a, b>,
divide: n ÷ m,
lambda: λx.A[x],
eq_int: (i =z j),
remainder: n rem m,
from-upto: [n, m),
add: n + m,
natural_number: $n
FDL editor aliases :
two-factorizations
Latex:
two-factorizations(n) == mapfilter(\mlambda{}a.<a, n \mdiv{} a>\mlambda{}a.(n rem a =\msubz{} 0);[1, n + 1))
Date html generated:
2016_05_15-PM-07_52_54
Last ObjectModification:
2015_09_23-AM-08_19_33
Theory : general
Home
Index