Nuprl Definition : sigmaset
Σa:A.B[a] == let T,f = A in <t:T × set-dom(B[f t]), λp.let t,s = p in (f t,set-item(B[f t];s))>
Definitions occuring in Statement :
orderedpairset: (a,b),
set-item: set-item(s;x),
set-dom: set-dom(s),
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
product: x:A × B[x]
Definitions occuring in definition :
apply: f a,
set-item: set-item(s;x),
orderedpairset: (a,b),
spread: spread def,
lambda: λx.A[x],
set-dom: set-dom(s),
product: x:A × B[x],
pair: <a, b>
FDL editor aliases :
sigmaset
Latex:
\mSigma{}a:A.B[a] == let T,f = A in <t:T \mtimes{} set-dom(B[f t]), \mlambda{}p.let t,s = p in (f t,set-item(B[f t];s))>
Date html generated:
2018_07_29-AM-10_04_06
Last ObjectModification:
2018_07_18-PM-03_43_50
Theory : constructive!set!theory
Home
Index