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