Nuprl Definition : dset_set
{x:s| Q[x]} == mk_dset({x:|s|| Q[x]} , =b)
Definitions occuring in Statement :
mk_dset: mk_dset(T, eq),
set_eq: =b,
set_car: |p|,
set: {x:A| B[x]}
Definitions occuring in definition :
mk_dset: mk_dset(T, eq),
set: {x:A| B[x]} ,
set_car: |p|,
set_eq: =b
Latex:
\{x:s| Q[x]\} == mk\_dset(\{x:|s|| Q[x]\} , =\msubb{})
Date html generated:
2016_05_15-PM-00_05_50
Last ObjectModification:
2015_09_23-AM-06_24_09
Theory : sets_1
Home
Index