Nuprl Definition : set_prod
s × t == mk_dset(|s| × |t|, λa,b. (a =b b))
Definitions occuring in Statement :
eq_pair: a =b b
,
mk_dset: mk_dset(T, eq)
,
set_car: |p|
,
lambda: λx.A[x]
,
product: x:A × B[x]
Definitions occuring in definition :
mk_dset: mk_dset(T, eq)
,
product: x:A × B[x]
,
set_car: |p|
,
lambda: λx.A[x]
,
eq_pair: a =b b
Latex:
s \mtimes{} t == mk\_dset(|s| \mtimes{} |t|, \mlambda{}a,b. (a =\msubb{} b))
Date html generated:
2016_05_15-PM-00_05_45
Last ObjectModification:
2015_09_23-AM-06_24_08
Theory : sets_1
Home
Index