Nuprl Definition : qadd_grp
<ℚ+> == <ℚ, λx,y. qeq(x;y), λx,y. q_le(x;y), λx,y. (x + y), 0, λx.-(x)>
Definitions occuring in Statement :
q_le: q_le(r;s),
qmul: r * s,
qadd: r + s,
rationals: ℚ,
qeq: qeq(r;s),
lambda: λx.A[x],
pair: <a, b>,
minus: -n,
natural_number: $n
Definitions occuring in definition :
rationals: ℚ,
qeq: qeq(r;s),
q_le: q_le(r;s),
qadd: r + s,
pair: <a, b>,
lambda: λx.A[x],
qmul: r * s,
minus: -n,
natural_number: $n
FDL editor aliases :
qadd_grp
Latex:
<\mBbbQ{}+> == <\mBbbQ{}, \mlambda{}x,y. qeq(x;y), \mlambda{}x,y. q\_le(x;y), \mlambda{}x,y. (x + y), 0, \mlambda{}x.-(x)>
Date html generated:
2016_05_15-PM-10_41_21
Last ObjectModification:
2015_09_23-AM-08_27_05
Theory : rationals
Home
Index