Nuprl Definition : vr_COMP
vr_COMP == 
F:
. 
P:
. x:. (x 
{x:| P x} 
(x = 0) 
F)
Definitions occuring in Statement :
nat: ,
prop: ,
all: x:A. B[x],
exists: x:A. B[x],
iff: P Q,
and: P Q,
member: t T,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
natural_number: $n,
equal: s = t
FDL editor aliases :
vr_COMP
vr\_COMP == \mforall{}F:\mBbbP{}. \mexists{}P:\mBbbN{} {}\mrightarrow{} \mBbbP{}. \mforall{}x:\mBbbN{}. (x \mmember{} \{x:\mBbbN{}| P x\} \mLeftarrow{}{}\mRightarrow{} (x = 0) \mwedge{} F)
Date html generated:
2012_02_20-PM-03_35_17
Last ObjectModification:
2012_02_02-PM-01_55_43
Home
Index