Nuprl Definition : int_loset
int_loset() == mk_oset(ℤ;λx,y. (x =z y);λx,y. x ≤z y)
Definitions occuring in Statement :
mk_oset: mk_oset(T;eq;leq),
le_int: i ≤z j,
eq_int: (i =z j),
lambda: λx.A[x],
int: ℤ
Definitions occuring in definition :
mk_oset: mk_oset(T;eq;leq),
int: ℤ,
eq_int: (i =z j),
lambda: λx.A[x],
le_int: i ≤z j
Latex:
int\_loset() == mk\_oset(\mBbbZ{};\mlambda{}x,y. (x =\msubz{} y);\mlambda{}x,y. x \mleq{}z y)
Date html generated:
2016_05_15-PM-00_05_57
Last ObjectModification:
2015_09_23-AM-06_24_10
Theory : sets_1
Home
Index