Nuprl Definition : posint_mul_mon
<ℤ+,*> == <ℕ+, λx,y. (x =z y), λx,y. x ≤z y, λx,y. (x * y), 1, λx.x>
Definitions occuring in Statement :
le_int: i ≤z j,
nat_plus: ℕ+,
eq_int: (i =z j),
lambda: λx.A[x],
pair: <a, b>,
multiply: n * m,
natural_number: $n
Definitions occuring in definition :
nat_plus: ℕ+,
eq_int: (i =z j),
le_int: i ≤z j,
multiply: n * m,
pair: <a, b>,
natural_number: $n,
lambda: λx.A[x]
Latex:
<\mBbbZ{}\msupplus{},*> == <\mBbbN{}\msupplus{}, \mlambda{}x,y. (x =\msubz{} y), \mlambda{}x,y. x \mleq{}z y, \mlambda{}x,y. (x * y), 1, \mlambda{}x.x>
Date html generated:
2016_05_16-AM-07_45_28
Last ObjectModification:
2015_09_23-AM-09_52_00
Theory : factor_1
Home
Index