Nuprl Definition : sq-id-fun
sq-id-fun(T) == x:T ⟶ {y:T| x ~ y}
Definitions occuring in Statement :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
sqequal: s ~ t
Definitions occuring in definition :
function: x:A ⟶ B[x],
set: {x:A| B[x]} ,
sqequal: s ~ t
FDL editor aliases :
sq-id-fun
Latex:
sq-id-fun(T) == x:T {}\mrightarrow{} \{y:T| x \msim{} y\}
Date html generated:
2016_05_13-PM-03_46_07
Last ObjectModification:
2015_09_22-PM-05_45_12
Theory : call!by!value_2
Home
Index